#5855: Computation Hangs Using PolyKinds
---------------------------------+------------------------------------------
Reporter: paf31 | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.4.1
Keywords: | Os: Windows
Architecture: Unknown/Multiple | Failure: Runtime crash
Difficulty: Unknown | Testcase:
Blockedby: | Blocking:
Related: |
---------------------------------+------------------------------------------
Changes (by simonpj):
* difficulty: => Unknown
Old description:
> 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.
New description:
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.
--
Comment:
(I've added some type signatures.)
Can you explain why you think the program should '''not''' diverge? That
is, why is this a bug?
Changing `compose` to use lazy pattern matching makes it converge:
{{{
compose ~(PHom f1 g1) ~(PHom f2 g2) = PHom (f2 . f1) (g2 . g1)
}}}
Simon
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/5855#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
