[Haskell-cafe] Fundeps and overlapping instances

[Etienne Laurin]

Hello,

2012/6/1 Iavor Diatchki <iavor.diatchki at gmail.com>:
> There is no problem if an instances uses a type family in it's
> assumption---the instances should be accepted only if GHC can see enough of
> the definition of the type family to ensure that the functional dependency
> holds.  This is exactly the same as what it would do to check that a super
> class constraint holds.

GHC cannot see enough of the definition because type families are
open. The type instances are not guaranteed to all be in scope when
the class instance is defined.

2012/6/1 AntC <anthony_clayden at clear.net.nz>:
> Some of Oleg's instances are awesome (and almost impenetrable -- the TTypeable
> code is a tour de force).
>
> It's all so *dys-functional* (IMO).

It's like a typed Prolog with a different order of evaluation.

> My take is that we should abandon Fundeps, and concentrate on introducing
> overlaps into type functions in a controlled way (what I've called 'dis-
> overlapped overlaps'.)

Abandoning fundeps would be a sad day for type-level programming.
There are many things other than overlaps that you can do with fundeps
and constraint kinds that you cannot currently do with type families,
such as:

- Partial application or higher-order programming.
- Short-circuit evaluation, lazy evaluation or type-level case.

To study the differences, I have been porting parts of the Prelude to
both type classes and type families.

http://code.atnnn.com/projects/type-prelude/repository/entry/Prelude/Type.hs
http://code.atnnn.com/projects/type-prelude/repository/entry/Prelude/Type/Families.hs

Etienne Laurin

> On Wed, May 30, 2012 at 11:14 PM, Etienne Laurin <etienne at atnnn.com> wrote:
>> > 1. Check that an instance is consistent with itself.  For example, this
>> > should be rejected:
>> >
>> > instance C a b
>> >
>> > because it allows C Int Bool and C Int Char which violate the functional
>> > dependency.
>>
>> This check may not always be as straightforward. When would this be a
>> valid instance?
>>
>> instance K a b ⇒ C a b
>>
>> With a few extra extensions, K could be a type family.
>>
>> C currently has the kind (a -> b -> Constraint), with no mention of
>> functional dependencies. Perhaps the kind of C should include the
>> functional dependencies of C?