New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Backwards state monad leads to cycle it type synonym declarations #94

Closed
jstolarek opened this Issue Sep 8, 2014 · 6 comments

Comments

Projects
None yet
2 participants
@jstolarek
Collaborator

jstolarek commented Sep 8, 2014

The backwards state monad, which I proudly announced during the talk to be promotable, fails to promote with "Cycle in type synonym declarations". After some very painful bisecting (because of th-desugar dependency) it turns out that this was introduced by th-desugar switch in be9c9cd

@jstolarek

This comment has been minimized.

Show comment
Hide comment
@jstolarek

jstolarek Sep 9, 2014

Collaborator

Oh, and here's the test code:

{-# LANGUAGE TemplateHaskell, KindSignatures, DataKinds, PolyKinds, TypeFamilies, UndecidableInstances, GADTs, AllowAmbiguousTypes #-}

module BackwardsStateMonad where

import Data.Singletons.TH
import Data.Singletons.Prelude


$(promote [d|
 data Nat = Zero | Succ Nat

 bind :: (Nat -> (Foo, Nat)) -> (Foo -> Nat -> (Foo, Nat)) -> (Nat -> (Foo, Nat))
 bind m k s2 = let (a,s0) = m s1
                   (b,s1) = k a s2
               in (b, s0)

 data Foo = Foo

 m :: Nat -> (Foo, Nat)
 m n = (Foo, Succ n)

 k :: Foo -> Nat -> (Foo, Nat)
 k a n = (a, Succ n)

 bar :: Nat -> (Foo, Nat)
 bar p = (bind m k) p

 |])

instance Show Nat where
   show Zero = "Zero"
   show (Succ n) = "Succ (" ++ show n ++ ")"

instance Show Foo where
   show _ = "Foo"

baz1a :: Proxy (Bar Zero)
baz1a = Proxy

baz1b :: Proxy '( 'Foo, Succ (Succ Zero))
baz1b = baz1a
Collaborator

jstolarek commented Sep 9, 2014

Oh, and here's the test code:

{-# LANGUAGE TemplateHaskell, KindSignatures, DataKinds, PolyKinds, TypeFamilies, UndecidableInstances, GADTs, AllowAmbiguousTypes #-}

module BackwardsStateMonad where

import Data.Singletons.TH
import Data.Singletons.Prelude


$(promote [d|
 data Nat = Zero | Succ Nat

 bind :: (Nat -> (Foo, Nat)) -> (Foo -> Nat -> (Foo, Nat)) -> (Nat -> (Foo, Nat))
 bind m k s2 = let (a,s0) = m s1
                   (b,s1) = k a s2
               in (b, s0)

 data Foo = Foo

 m :: Nat -> (Foo, Nat)
 m n = (Foo, Succ n)

 k :: Foo -> Nat -> (Foo, Nat)
 k a n = (a, Succ n)

 bar :: Nat -> (Foo, Nat)
 bar p = (bind m k) p

 |])

instance Show Nat where
   show Zero = "Zero"
   show (Succ n) = "Succ (" ++ show n ++ ")"

instance Show Foo where
   show _ = "Foo"

baz1a :: Proxy (Bar Zero)
baz1a = Proxy

baz1b :: Proxy '( 'Foo, Succ (Succ Zero))
baz1b = baz1a

@goldfirere goldfirere added the invalid label Sep 16, 2015

@goldfirere

This comment has been minimized.

Show comment
Hide comment
@goldfirere

goldfirere Sep 16, 2015

Owner

Now it just loops. But getting this to work out means that we need to have a real semantics for type family reduction, which GHC doesn't have. Until GHC catches up, this is a non-starter. But I'm not even going to label this as blocked upstream, because there's no plans to give GHC a well-defined semantics for type families in the near future. So I'm just closing this ticket as invalid, as we're trying to do something that GHC fundamentally doesn't support.

Owner

goldfirere commented Sep 16, 2015

Now it just loops. But getting this to work out means that we need to have a real semantics for type family reduction, which GHC doesn't have. Until GHC catches up, this is a non-starter. But I'm not even going to label this as blocked upstream, because there's no plans to give GHC a well-defined semantics for type families in the near future. So I'm just closing this ticket as invalid, as we're trying to do something that GHC fundamentally doesn't support.

@goldfirere goldfirere closed this Sep 16, 2015

@jstolarek

This comment has been minimized.

Show comment
Hide comment
@jstolarek

jstolarek Sep 17, 2015

Collaborator

But remember that this used to work.

Collaborator

jstolarek commented Sep 17, 2015

But remember that this used to work.

@goldfirere

This comment has been minimized.

Show comment
Hide comment
@goldfirere

goldfirere Sep 17, 2015

Owner

Yes, but I think that was as much of an accident as this is. And note that it worked on 7.8, so it's possible that my updates would make it work on 7.8 (if it compiled at all). There's a pretty big change in the way that type families reduce between 7.8 and 7.10.

Owner

goldfirere commented Sep 17, 2015

Yes, but I think that was as much of an accident as this is. And note that it worked on 7.8, so it's possible that my updates would make it work on 7.8 (if it compiled at all). There's a pretty big change in the way that type families reduce between 7.8 and 7.10.

@jstolarek

This comment has been minimized.

Show comment
Hide comment
@jstolarek

jstolarek Sep 17, 2015

Collaborator

There's a pretty big change in the way that type families reduce between 7.8 and 7.10.

Where can I read more about this? Is there a ticket or a wiki page?

Collaborator

jstolarek commented Sep 17, 2015

There's a pretty big change in the way that type families reduce between 7.8 and 7.10.

Where can I read more about this? Is there a ticket or a wiki page?

@goldfirere

This comment has been minimized.

Show comment
Hide comment
@goldfirere

goldfirere Sep 17, 2015

Owner

No. It was all meant to be under-the-hood. But it's quite conceivable that this sort of weirdness would change in behavior. It was done while fixing up how Coercible is solved.

Owner

goldfirere commented Sep 17, 2015

No. It was all meant to be under-the-hood. But it's quite conceivable that this sort of weirdness would change in behavior. It was done while fixing up how Coercible is solved.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment