Recursive algebraic data types through polymorphism in Haskell

Question

I am trying to understand the definition, de- and coding of recursive algebraic data types given the functionality of universal polymorphism. As an example, I tried to implement a recursive type of binary trees through

data BTAlg x = Empty | Leaf xx type BT = forall z. ((BTAlg z) -> z) -> z 

the intuition is that the type of binary trees must be initial among all types T equipped with the constant e: T and the binary operation m: T -> T -> T , that is, the "initial module" over the functor BTAlg . In other words, the BT element is an assignment method for any such module T element T

The module structure on BT itself can be determined through

 initial_module :: (BTAlg BT) -> BT initial_module = \s -> case s of Empty -> (\f -> (f Empty)) Leaf xy -> (\f -> (f (Leaf (xf) (yf)))) 

As a step towards pattern matching for BT , now I want to apply the x:BT element to the BT type, which I consider to be some kind of encoding-decoding of x .

 decode_encode :: BT -> BT decode_encode x = x initial_module 

However, this code leads to a type error that I cannot handle:

 Couldn't match expected type `(BTAlg z -> z) -> z' with actual type `BT' Expected type: BTAlg ((BTAlg z -> z) -> z) -> (BTAlg z -> z) -> z Actual type: BTAlg BT -> (BTAlg z0 -> z0) -> z0 In the first argument of `x', namely `initial_module' In the expression: x initial_module 

What is wrong here? I do not know why the type checker does not recognize that the parameter of the universal type z must be specialized for BT in x , so that x applicable to initial_module ; writing (x :: ((BTAlg BT) -> BT) -> BT) initial_module doesn't help either.

Addendum regarding motivation for defining decode_encode : I want to convince myself that BT is actually “isomorphic” to the standard implementation

 data BTStd = StdEmpty | StdLeaf BTStd BTStd 

binary trees; while I don’t know how to do it exactly inside Haskell, the starter would be to build BT -> BTStd and BTStd -> BT cards going back and forth between the two implementations.

Definition of toStandard: BT -> BTStd is an application of the universal BT property to the canonical structure of the BTAlg module on BTStd :

 std_module :: (BTAlg BTStd) -> BTStd std_module s = case s of Empty -> StdEmpty Leaf xy -> StdLeaf xy toStandard: BT -> BTStd toStandard x = x std_module 

For the decoding function fromStandard: BTStd -> BT I would like to do the following:

 fromStandard :: BTStd -> BT fromStandard s = case s of StdEmpty -> initial_module Empty StdLeaf xy -> initial_module (Leaf (fromStandard x) (fromStandard y)) 

However, this gives the same typing problems as the direct definition of decode_encode above:

 Couldn't match expected type `BT' with actual type `(BTAlg z0 -> z0) -> z0' In the return type of a call of `fromStandard' Probable cause: `fromStandard' is applied to too few arguments In the first argument of `Leaf', namely `(fromStandard x)' In the first argument of `initial_module', namely `(Leaf (fromStandard x) (fromStandard y))' 

Thanks!

Answer 1

If you look at the output type for decode_encode

 :t decode_encode > decode_encode :: ((BTAlg BT -> (BTAlg z -> z) -> z) -> t) -> t 

it is clear that the GHC has lost quite a bit of polymorphism. I'm not quite sure about the details here - this code requires ImpredicativeTypes to compile, which usually occurs when my understanding starts to break down. However, there is a standard way to preserve polymorphism: use newtype

 newtype BT = BT { runBT :: forall z. (BTAlg z -> z) -> z } 

newtype establishes the isomorphism BT ~ forall z . (BTAlg z -> z) -> z BT ~ forall z . (BTAlg z -> z) -> z , attested by BT and runBT . As long as we put these witnesses in the right places, we can move forward.

 data BTAlg x = Empty | Leaf xx data BTStd = StdEmpty | StdLeaf BTStd BTStd newtype BT = BT { runBT :: forall z. ((BTAlg z) -> z) -> z } initial_module :: BTAlg BT -> BT initial_module s = case s of Empty -> BT $ \f -> (f Empty) Leaf xy -> BT $ \f -> (f (Leaf (runBT xf) (runBT yf))) std_module :: (BTAlg BTStd) -> BTStd std_module s = case s of Empty -> StdEmpty Leaf xy -> StdLeaf xy toStandard :: BT -> BTStd toStandard x = runBT x std_module fromStandard :: BTStd -> BT fromStandard s = case s of StdEmpty -> initial_module Empty StdLeaf xy -> initial_module (Leaf (fromStandard x) (fromStandard y)) 

In particular, it’s good that we use runBT to control when and how many times the lambda type is used in BT

 decode_encode :: BT -> BT decode_encode x = runBT x initial_module 

One use of runBT corresponds to one unification of the quantified type.