[Haskell-cafe] type families and type signatures

[Claus Reinke]

>> To make it legal: If foo' with a type signature doesn't type check,  
>> try to infer a type without a signature.  If this succeeds then  
>> check that the type that was inferred is alpha-convertible to the  
>> original signature.  If it is, accept foo'; the signature doesn't  
>> add any information.
> 
> This harder, if not impossible.  What does it mean for two signatures  
> to be "alpha-convertible"? 
>
> ..[type synonym expansion vs type synonym family reduction]
>
> So, I guess, you don't really mean alpha-convertible in its original  
> syntactic sense.  We should accept the definition if the inferred and  
> the given signature are in some sense "equivalent".  For this  
> "equivalence" to be robust, I am sure we need to define it as follows,  
> where <= is standard type subsumption:
> 
>   t1 "equivalent" t2  iff   t1 <= t2 and t2 <= t1

i would like to express my doubts about this assumption (which
relates directly to the earlier discussion about subsumption).

no matter what subsumption or what semantic equivalence we
are talking about, we expect it to *include* syntactic identity
(reflexivity of the relations):

    forall t: t <= t
    forall t: t ~ t

moving some equational theory into the "syntactic" equivalence
does not imply that syntactic has to be the full semantic 
equivalence - as the example of alpha- vs beta+alpha-
convertibility in lambda calculus demonstrates, it is convenient
to be able to ignore some representational issues when talking
about "identical" terms in the greater theory.

it would help to do the same here, and distinguish between
a syntactic and a semantic equivalence of types, where the
latter includes and extends the former:

syntactic: alpha-conversion, permutation of contexts,
    probably type synonym expansion (because they are 
    treated as syntactic macros, outside the theory)

semantic: type family reduction, ..

i'm tempted to the conclusion that the inability of the current
system to check its inferred signatures means that reflexivity
(of type subsumption/equivalence) is violated: if two types
are the same, they should be equivalent and subsume each
other. i can't see how the theory can work without this?

> However, the fact that we cannot decide type subsumption 
> for ambiguous types is exactly what led us to the original 
> problem.  So, nothing has been won.

imho, the trick is to separate syntactic and semantic
equivalence, even if we include some "modulo theory"
in the former. both <= and ~ need to include this
syntactic equivalence. but syntactic equivalence should
remain straightforward to check - nothing should be
included in it that isn't easily checkable.

claus

ps i hope it is obvious that i'd like infered signatures to
    be checkable, not non-checkable signatures to be
    rejected?-)