Are type synonym families really equivalent to fundeps?
The following code builds and appears to work great (assuming one allows undecidable instances). I have tried both a natural translation into type synonym families, and also the mechanical transformation in http://www.cse.unsw.edu.au/~chak/papers/tyfuns.pdf -- but I can't get either to work. The two fishy things are: 1. There is a functional dependency (a -> t) in the original. Actually, this isn't always true since t is sometimes not uniquely determined by a; but GHC always seems to do the right thing anyway. There doesn't seem to be any way to "cheat" like this with type families. 2. In the second and fourth instances, the type variable x appears twice in the parameters of the type function built from the fundep (a b -> c). This causes an error. If I try adding (x ~ x') to the context and making one of them x' instead of x, I get different errors. I'm starting to this this is an example of using functional dependencies that has no translation to type families. Can anyone free me of such thoughts? Code with fundeps is: data Var a = Var Int (Maybe String) data RHS a b = RHS a b class Action t a b c | a -> t, a b -> c, a c -> b instance Action t () y y instance Action t (Var x) (x -> y) y instance Action t [t] y y instance (Action t a b c) => Action t (RHS (Var x) a) (x -> b) c instance (Action t a b c) => Action t (RHS [t] a) b c -- Chris Smith
Chris Smith wrote:
The following code builds and appears to work great (assuming one allows undecidable instances). I have tried both a natural translation into type synonym families, and also the mechanical transformation in http://www.cse.unsw.edu.au/~chak/papers/tyfuns.pdf -- but I can't get either to work.
I _just_ read that. Let's see how I do:
The two fishy things are:
1. There is a functional dependency (a -> t) in the original. Actually, this isn't always true since t is sometimes not uniquely determined by a; but GHC always seems to do the right thing anyway. There doesn't seem to be any way to "cheat" like this with type families.
I will go out on a limb and guess that GHC accepts your uses of the instances below for reasons similar to the fact that GHC sometimes accepts overlapping instances. GHC only lazily reports an overlapping instances error when it detect concrete usage of the instances that fall into the overlapping "zone". Note that Hugs checks eagerly. (I ran into this difference in the older version of regex-base's RegexContext instances. GHC was okay but Hugs complained). My guess is that: if every time GHC sees a == () you also always use the same type 't' then GHC might not complain about it. If you _actually_ fool GHC then you should file a bug.
2. In the second and fourth instances, the type variable x appears twice in the parameters of the type function built from the fundep (a b -> c). This causes an error. If I try adding (x ~ x') to the context and making one of them x' instead of x, I get different errors.
I'm starting to this this is an example of using functional dependencies that has no translation to type families. Can anyone free me of such thoughts?
Code with fundeps is:
data Var a = Var Int (Maybe String) data RHS a b = RHS a b
class Action t a b c | a -> t, a b -> c, a c -> b instance Action t () y y instance Action t (Var x) (x -> y) y instance Action t [t] y y instance (Action t a b c) => Action t (RHS (Var x) a) (x -> b) c instance (Action t a b c) => Action t (RHS [t] a) b c
I have never used associated types or type families. I assume you cannot rely
on GHC lazy goodwill for the a->t constraint. You will have to be explicit.
Not using associated types but type families I think the syntax should be:
-- No obvious need for kind annotations, so this is
type family A_T a
type family A_B_C a b
type family A_C_B a c
-- The name are
-- You need to help GHC more here:
type instance A_T () =
Ah... I see that I have a bug in my proposal, perhaps corrected below.
2. In the second and fourth instances, the type variable x appears twice in the parameters of the type function built from the fundep (a b -> c). This causes an error. If I try adding (x ~ x') to the context and making one of them x' instead of x, I get different errors.
I see the problem with the x parameter now:
I'm starting to this this is an example of using functional dependencies that has no translation to type families. Can anyone free me of such thoughts?
Code with fundeps is:
data Var a = Var Int (Maybe String) data RHS a b = RHS a b
class Action t a b c | a -> t, a b -> c, a c -> b instance Action t () y y instance Action t (Var x) (x -> y) y instance Action t [t] y y instance (Action t a b c) => Action t (RHS (Var x) a) (x -> b) c instance (Action t a b c) => Action t (RHS [t] a) b c
I have never used associated types or type families. I assume you cannot rely on GHC lazy goodwill for the a->t constraint. You will have to be explicit. Not using associated types but type families I think the syntax should be:
[snip]
type instance A_C_B (RHS (Var x) a) c = x -> A_C_B a c
The above is the corrected line. I had forgotten the (x->) on the RHS.
[snip]
There is are two oddities with your example that I am confused by.
Code with fundeps is:
data Var a = Var Int (Maybe String) data RHS a b = RHS a b
class Action t a b c | a -> t, a b -> c, a c -> b
instance Action t () y y instance Action t (Var x) (x -> y) y instance (Action t a b c) => Action t (RHS (Var x) a) (x -> b) c instance (Action t a b c) => Action t (RHS [t] a) b c
Any of the the above for instances makes GHC 6.6.1 complain without adding -fallow-undecidable-instances which makes your code a poor test of whether fundeps are translatable to standard type families or associated types. The following instance does not make GHC complain about undecidable instances:
instance Action t [t] y y
The second oddity is in the last two lines. Why not this:
instance (Action tNew a b c) => Action t (RHS (Var x) a) (x -> b) c
instance (Action tNew a b c) => Action t (RHS [t] a) b c
where the t in the constraint is _not_ the t in the instance head. By making
the 't' the same you are also declaring that
A_T a ~ A_T (RHS (Var x) a)
and
A_T a ~ A_T (RHS [t] a)
are going to need to hold. By using tNew this is not required to hold.
I think one can change my earlier proposal to include this, but there are zero
examples of this syntax, so I am likely making up some syntax that does not exist:
type instance (A_T a ~ A_T (RHS (Var x) a)) => A_B_C (RHS (Var x) a) (x->b) =
A_B_C a b
type instance (A_T a ~ A_T (RHS (Var x) a)) => A_C_B (RHS (Var x) a) c = x ->
A_C_B a c
type instance (A_T a ~ A_T (RHS [t] a)) => A_B_C (RHS [t] a) b = A_B_C a b
type instance (A_T a ~ A_T (RHS [t] a)) => A_C_B (RHS [t] a) c = A_C_B a c
With the rest unchanged:
type family A_T a
type family A_B_C a b
type family A_C_B a c
-- You need to help GHC more here:
type instance A_T () =
I think one can change my earlier proposal to include this, but there are zero examples of this syntax, so I am likely making up some syntax that does not exist:
type instance (A_T a ~ A_T (RHS (Var x) a)) => A_B_C (RHS (Var x) a) (x->b) = A_B_C a b
type instance (A_T a ~ A_T (RHS (Var x) a)) => A_C_B (RHS (Var x) a) c = x -> A_C_B a c
type instance (A_T a ~ A_T (RHS [t] a)) => A_B_C (RHS [t] a) b = A_B_C a b type instance (A_T a ~ A_T (RHS [t] a)) => A_C_B (RHS [t] a) c = A_C_B a c
I am afraid you are right: this syntax does not exist. Type family instances cannot have a context. They are unconditional. Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be
ChrisK wrote:
-- You need to help GHC more here: type instance A_T () =
type instance A_T (Var x) = type instance A_T [t] = t type instance A_T (RHS (Var x) a) = type instance A_T (RHS [t] a) = t
Chris, this actually isn't workable. The problem is that there is no such thing as "explicit type you actually ue with ()". If the type variable 'a' gets matched to () or (Var x), then t can be any type. That works currently. I don't want to fix the type of 't', as this code goes in a library where different applications are using different types for 't'. As I said, this is probably not really right, since () really doesn't determine a value for a; but it does work right now. Just for kicks, I tried this: type instance A_T () = forall t. t it didn't work. -- Chris Smith
Chris Smith wrote,
ChrisK wrote:
-- You need to help GHC more here: type instance A_T () =
type instance A_T (Var x) = type instance A_T [t] = t type instance A_T (RHS (Var x) a) = type instance A_T (RHS [t] a) = t Chris, this actually isn't workable. The problem is that there is no such thing as "explicit type you actually ue with ()". If the type variable 'a' gets matched to () or (Var x), then t can be any type. That works currently. I don't want to fix the type of 't', as this code goes in a library where different applications are using different types for 't'.
As I said, this is probably not really right, since () really doesn't determine a value for a; but it does work right now.
Just for kicks, I tried this:
type instance A_T () = forall t. t
it didn't work.
Right-hand sides of type instances may not be polytypes. There is a counter example in Section 7.2, http://haskell.org/haskellwiki/GHC/Type_families but the text didn't explicitly make that point. I edited it to include that. Cheers, Manuel
Thanks for this interesting example. Just le me say up front that I regard any FD program that you cannot translate to type families as a bug in the TF implementation. To qualify this a little, this is definitely so for programs that do not require undecidable instances. With undecidable instances, it is anybodys guess what the actual semantics of the FD program is, so trying to approximate that unknown behaviour with an TF program is necessarily partly guesswork, or a matter of reading GHC source code. Chris Smith wrote,
The following code builds and appears to work great (assuming one allows undecidable instances). I have tried both a natural translation into type synonym families, and also the mechanical transformation in http://www.cse.unsw.edu.au/~chak/papers/tyfuns.pdf -- but I can't get either to work.
The two fishy things are:
1. There is a functional dependency (a -> t) in the original. Actually, this isn't always true since t is sometimes not uniquely determined by a; but GHC always seems to do the right thing anyway. There doesn't seem to be any way to "cheat" like this with type families.
From your example code, it is entirely unclear why you need the (a -> t) dependence at all. You only provided the class and instances declarations, and those (not surprisingly) compile fine without that dependency. Can you give an example that does not work if we leave that dependency out?
2. In the second and fourth instances, the type variable x appears twice in the parameters of the type function built from the fundep (a b -> c). This causes an error. If I try adding (x ~ x') to the context and making one of them x' instead of x, I get different errors.
Currently, the TF implementation requires type instances to be left-linear (ie, no repeated type variables in the head). I actually think we can lift that restriction, but for the time being adding an equality to the context is a sensible work around. Leaving out the (a -> t) dependency (whose purpose I don't understand) and using equalities to circumvent the restriction to left-linear heads, the program translates to data Var a = Var Int (Maybe String) data RHS a b = RHS a b class (C a b ~ c, B a c ~ b) => Action t a b c where type C a b type B a c instance Action t () y y where type C () y = y type B () y = y instance (x ~ x') => Action t (Var x) (x' -> y) y where type C (Var x) (x' -> y) = y type B (Var x) y = x -> y instance Action t [t] y y where type C [t] y = y type B [t] y = y instance (Action t a b c, x ~ x') => Action t (RHS (Var x) a) (x' -> b) c where type C (RHS (Var x) a) (x' -> b) = C a b type B (RHS (Var x) a) c = x -> B a c instance (Action t a b c) => Action t (RHS [t] a) b c where type C (RHS [t] a) b = C a b type B (RHS [t] a) c = B a c This program is currently also rejected due to a bug in the treatment of equalities in superclass constraints. We already tripped over that in the context of another program, and I believe Tom Schrijvers is currently working at fixing it. A nice aspect of the above TF version of this code is that (if I am not mistaken) it does *not* require undecidable instances. Manuel
Code with fundeps is:
data Var a = Var Int (Maybe String) data RHS a b = RHS a b
class Action t a b c | a -> t, a b -> c, a c -> b instance Action t () y y instance Action t (Var x) (x -> y) y instance Action t [t] y y instance (Action t a b c) => Action t (RHS (Var x) a) (x -> b) c instance (Action t a b c) => Action t (RHS [t] a) b c
participants (4)
-
Chris Smith -
ChrisK -
Manuel M T Chakravarty -
Tom Schrijvers