TypeFamilies vs. FunctionalDependencies & type-level recursion

[AntC]

Simon Peyton-Jones <simonpj at ...> writes:

> 
> No I didn't intend to put more in the header, perhaps less.
> I've added more clarification.  
> 
> Simon

Thanks Simon, I agree with keeping it terse; I agree with your "yuk" rating 
for `of'. At risk of bikeshedding over surafce syntax (for a feture that's 
still only a gleam in the eye) ...

I think we're going to see two idioms for overlapping instances:

Idiom 1: total instance (this would apply to all the HList examples). We only 
need one instance group for the whole; then it's the type family decl that 
seems superfluous. Perhaps we could allow:

    type family Equal a b :: Bool where
        Equal a a = True
        Equal a b = False

    type family HasMember a (b :: '[]) :: Bool where
        HasMember a '[] = False                      -- (not overlapping)
        HasMember a ( a ': bs ) = True
        HasMember a ( b ': bs ) = HasMember a bs

Idiom 2: an instance group discriminated by the outermost type constructor, or 
by one of the arguments (this might apply for Monad Transformers). Then 
although the instance header is superfluous, it might be useful documentation:

    module SomeLibrary where
        type family F a b :: ...

    module MyModule where
        data MyType = ...
        type instance F MyType b where    -- total function for a ~ MyType
            F MyType Int = ...
            F MyType (Int, b) = ...
            F MyType b = ...

AntC