[Haskell-cafe] checking types with type families
simonpj at microsoft.com
Wed Jul 7 17:14:31 EDT 2010
Martin Sulzmann, Jeremy Wazny<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/w/Wazny:Jeremy.html>, Peter J. Stuckey<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/s/Stuckey:Peter_J=.html>: A Framework for Extended Algebraic Data Types. FLOPS 2006<http://www.informatik.uni-trier.de/%7Eley/db/conf/flops/flops2006.html#SulzmannWS06>: 47-64
describes such a system, fully implemented in Chameleon, but this
system is no longer maintained.
Type families and Fundeps are equivalent in expressive power and it's
not too hard to show how to encode one in terms of the other.
Local constraints are an orthogonal extension. In terms of type inference,
type families + local constraints and fundeps + local constraints pose the same
Probably, Simon is refrerring to the 'unresolved' issue of providing a System F style translation for fundeps + local constraints.
Apologies, Martin, you are quite right. Indeed, you were the first to teach me about implication constraints, which are the key to combining local constraints and functional dependencies. Chameleon implements such a system, using (I believe) the Constraint Handling Rule framework to solve the resulting constraints.
However as you mention we could not figure out a good way to combine this approach to constraint solving with evidence generation, although it seems that in principle it should be possible. As you say
Well, the point is that System FC
is geared toward type families. The two possible solutions are (a) either
consider fundeps as syntactic sugar for type families (doesn't quite work once
you throw in overlapping instances), (b) design a variant System FC_fundep
which has built-in support for fundeps.
Why is FC is geared towards type families? It's not an accidental bias; it's more that I know how to do (a) and I don't know how to do (b).
I'll write separately about the issue of overlap
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe