Equality constraints (~): type-theory behind them

[Anthony Clayden]

The (~) constraint syntax is enabled by either `GADTs` or `TypeFamilies`
language extension.

GADTs/Assoc Data Types/Assoc Type Synonyms/Type Families arrived in a
series of papers 2005 to 2008, and IIRC the development wasn't finished in
full in GHC until after that. (Superclass constraints took up to about
2010.)

Suppose I wanted just the (~) parts of those implementations. Which would
be the best place to look? (The Users Guide doesn't give a reference.) ICFP
2008 'Type Checking with Open Type Functions' shows uses of (~) in
user-written code, but doesn't explain it or motivate it as a separate
feature.

My specific question is: long before (~), it was possible to write a
TypeCast class, with bidirectional FunDeps to improve each type parameter
from the other. But for the compiler to see the type improvement at term
level, typically you also need a typeCast method and to explicitly wrap a
term in it. If you just wrote a term of type `a` in a place where `b` was
wanted, the compiler would either fail to see your `TypeCast a b`, or unify
the two too eagerly, then infer an overall type that wasn't general enough.

(For that reason, the instance for TypeCast goes through some
devious/indirect other classes/instances or exploits separate compilation,
to hide what's going on from the compiler's enthusiasm.)

But (~) does some sort of magic: it's a kinda typeclass but without a
method. How does it mesh with type improvement in the goldilocks zone:
neither too eager nor too lazy?


AntC
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20181207/ef688330/attachment.html>