Are type synonym families really equivalent to fundeps?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
8 messages Options
Reply | Threaded
Open this post in threaded view
|

Are type synonym families really equivalent to fundeps?

Chris Smith-39
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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Are type synonym families really equivalent to fundeps?

haskell-2
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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Are type synonym families really equivalent to fundeps?

haskell-2
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]

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Are type synonym families really equivalent to fundeps?

haskell-2
In reply to this post by haskell-2
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.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Are type synonym families really equivalent to fundeps?

Chris Smith-39
In reply to this post by haskell-2
ChrisK wrote:
> -- 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

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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Are type synonym families really equivalent to fundeps?

Manuel M T Chakravarty
In reply to this post by Chris Smith-39
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
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Are type synonym families really equivalent to fundeps?

Manuel M T Chakravarty
In reply to this post by Chris Smith-39
Chris Smith wrote,

> ChrisK wrote:
>> -- 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
>
> 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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Are type synonym families really equivalent to fundeps?

Tom Schrijvers-2
In reply to this post by haskell-2
> 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: [hidden email]
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe