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

[ChrisK]

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 () = <explicit type you actually use with ()>
type instance A_T (Var x) = <explicit type you actually use with (Var x)>
type instance A_T [t] = t
type instance A_T (RHS (Var x) a) = <explicit type you actually use ...>
type instance A_T (RHS [t] a) = t

-- These two seem easy to write and seem to follow the rules in the paper:
type instance A_B_C () y = y
type instance A_B_C (Var x) (x->y) = y
type instance A_B_C [t] y = y

type instance A_C_B () y = y
type instance A_C_B (Var x) y = x->y
type instance A_C_B [t] y = y

One could also manually simplify the right hand side of the ~ constraints by
using the A_T instances.