[Haskell-cafe] Are type synonym families really equivalent to fundeps?

[Manuel M T Chakravarty]

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
>