#5855: Computation Hangs Using PolyKinds
---------------------------+------------------------------------------------
Reporter: paf31 | Owner:
Type: bug | Status: new
Priority: normal | Component: Compiler
Version: 7.4.1 | Keywords:
Os: Windows | Architecture: Unknown/Multiple
Failure: Runtime crash | Testcase:
Blockedby: | Blocking:
Related: |
---------------------------+------------------------------------------------
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 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 f1 g1) (PHom f2 g2) = PHom (f2 . f1) (g2 . g1)
> 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.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/5855>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
