Hi all, I have a data type looking like this: data Foo e a where Foo :: e → Foo e a I would like to instantiate it to make it equivalent to: data Bar a where A :: String → Bar Int B :: Maybe a → Bar a How can I do that? With a functional dependency? I probably need to change the definition of Foo.
Hello, I would say that type families should do the joke: {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE GADTs #-} type family Prod a where Prod String = Int Prod (Maybe a) = a data Foo e a where Foo :: e -> Foo (Prod e) a Regards. 2016-07-04 22:43 GMT+02:00 Corentin Dupont <corentin.dupont@gmail.com>:
Hi all, I have a data type looking like this:
data Foo e a where
Foo :: e → Foo e a
I would like to instantiate it to make it equivalent to:
data Bar a where
A :: String → Bar Int B :: Maybe a → Bar a
How can I do that? With a functional dependency? I probably need to change the definition of Foo.
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
I'll add that Gautier's Prod has an inverse. When it's included, ghc can infer the types of x in these expressions: \x -> (Foo x :: Foo Int a) \x -> (Foo x :: Foo String a) as String and Maybe String respectively. Prod was unchanged, but the rest becomes: type family ProdInv a where ProdInv Int = String ProdInv a = Maybe a data Foo e a where Foo :: e ~ ProdInv (Prod e) => e -> Foo (Prod e) a I also thought about using a data family instead of a pair of type families. But then you still have two constructors. `class ProdFD e pe | e -> pe, pe -> e` can't work: 1. FDs don't provide coercions like TFs 2. the two ProdFD instances are rejected -- they overlap/violate FDs On Mon, Jul 4, 2016 at 5:31 PM, Gautier DI FOLCO <gautier.difolco@gmail.com> wrote:
Hello,
I would say that type families should do the joke:
{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE GADTs #-} type family Prod a where Prod String = Int Prod (Maybe a) = a
data Foo e a where
Foo :: e -> Foo (Prod e) a
Regards.
2016-07-04 22:43 GMT+02:00 Corentin Dupont <corentin.dupont@gmail.com>:
Hi all, I have a data type looking like this:
data Foo e a where
Foo :: e → Foo e a
I would like to instantiate it to make it equivalent to:
data Bar a where
A :: String → Bar Int B :: Maybe a → Bar a
How can I do that? With a functional dependency? I probably need to change the definition of Foo.
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
participants (3)
-
adam vogt -
Corentin Dupont -
Gautier DI FOLCO