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

[ChrisK]

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 () = <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_B_C (RHS (Var x) a) (x->b) = A_B_C a b
type instance A_B_C (RHS [t] a) b = A_B_C a b

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
type instance A_C_B (RHS (Var x) a) c = A_C_B a c
type instance A_C_B (RHS [t] a) c = A_C_B a c

-- If you need kind annotations then you should use edited versions of these
-- instead of what I gave above:
type family A_T (a :: *) :: *
type family A_B_C (a :: *) (b :: *) :: *
type family A_C_B (a :: *) (c :: *) :: *

Does this work?

Cheers,
  Chris