Computation Hangs Using PolyKinds
I have tried to distill this down to a minimal example. The following computation hangs in ghci when evaluating "toInt Zero":
> {-# LANGUAGE GADTs, DataKinds, PolyKinds, KindSignatures #-}
> data Choice = Fst | Snd
> data PHom p1 p2 = PHom (p1 Fst -> p2 Fst) (p1 Snd -> p2 Snd)
> data FNat :: (Choice -> *) -> Choice -> * where
> FZero :: FNat p Fst
> FSucc1 :: p Snd -> FNat p Fst
> FSucc2 :: p Fst -> FNat p Snd
> hmap :: PHom t p -> PHom (FNat t) (FNat p)
> hmap (PHom f g) = PHom hf hg where
> hf FZero = FZero
> hf (FSucc1 x) = FSucc1 (g x)
> hg (FSucc2 x) = FSucc2 (f x)
> data Nat :: Choice -> * where
> Zero :: Nat Fst
> Succ1 :: Nat Snd -> Nat Fst
> Succ2 :: Nat Fst -> Nat Snd
> out = PHom f g where
> f Zero = FZero
> f (Succ1 n) = FSucc1 n
> g (Succ2 n) = FSucc2 n
> compose :: PHom p1 t -> PHom t p2 -> PHom p1 p2
> compose (PHom f1 g1) (PHom f2 g2) = PHom (f2 . f1) (g2 . g1)
> fold :: PHom (FNat p) p -> PHom Nat p
> fold phi = compose out (compose (hmap (fold phi)) phi)
> data EvenOdd :: Choice -> * where
> Even :: Int -> EvenOdd Fst
> Odd :: Int -> EvenOdd Snd
> toInt :: Nat Fst -> Int
> toInt x =
> let (PHom f g) = fold (PHom phi psi) in
> let (Even n) = f x in n where
> phi FZero = Even 0
> phi (FSucc1 (Odd n)) = Even (n + 1)
> psi (FSucc2 (Even n)) = Odd (n + 1)
Setting a breakpoint in ghci seems to indicate that the expression (fold (PHom phi psi)) is being evaluated in full, which would obviously cause an unbounded recursion.
However, the following version runs fine and terminates as expected:
> {-# LANGUAGE GADTs, DataKinds, PolyKinds, KindSignatures, RankNTypes #-}
> data Choice = Fst | Snd
> newtype PHom p1 p2 = PHom { runPHom :: forall r. ((p1 Fst -> p2 Fst) -> (p1 Snd -> p2 Snd) -> r) -> r }
> mkPHom f g = PHom (\h -> h f g)
> fstPHom p = runPHom p (\f -> \g -> f)
> sndPHom p = runPHom p (\f -> \g -> g)
> data FNat :: (Choice -> *) -> Choice -> * where
> FZero :: FNat p Fst
> FSucc1 :: p Snd -> FNat p Fst
> FSucc2 :: p Fst -> FNat p Snd
> hmap p = mkPHom hf hg where
> hf FZero = FZero
> hf (FSucc1 x) = FSucc1 (sndPHom p x)
> hg (FSucc2 x) = FSucc2 (fstPHom p x)
> data Nat :: Choice -> * where
> Zero :: Nat Fst
> Succ1 :: Nat Snd -> Nat Fst
> Succ2 :: Nat Fst -> Nat Snd
> out = mkPHom f g where
> f Zero = FZero
> f (Succ1 n) = FSucc1 n
> g (Succ2 n) = FSucc2 n
> compose f g = mkPHom (fstPHom g . fstPHom f) (sndPHom g . sndPHom f)
> fold phi = compose out (compose (hmap (fold phi)) phi)
> data EvenOdd :: Choice -> * where
> Even :: Int -> EvenOdd Fst
> Odd :: Int -> EvenOdd Snd
> toInt :: Nat Fst -> Int
> toInt x =
> let p = fold (mkPHom phi psi) in
> let (Even n) = fstPHom p x in n where
> phi FZero = Even 0
> phi (FSucc1 (Odd n)) = Even (n + 1)
> psi (FSucc2 (Even n)) = Odd (n + 1)
The major change is that the data type PHom has been replaced with a newtype wrapper around a product encoded as a function.