[Haskell-cafe] checking types with type families

[Martin Sulzmann]

On Thu, Jul 1, 2010 at 7:54 PM, Simon Peyton-Jones <simonpj at microsoft.com>wrote:

>
> |  Also, what is the difference between fundeps and type families
> |  wrt local type constraints? I had always assumed them to be
> |  equivalent, if fully implemented. Similar to logic vs functional
> |  programming, where Haskellers tend to find the latter more
> |  convenient. Functional logic programming shows that there
> |  are some tricks missing if one just drops the logic part.
>
> Until now, no one has know how to combine fundeps and local constraints.
>  For example
>
>  class C a b | a->b where
>    op :: a -> b
>
>   instance C Int Bool where
>     op n = n>0
>
>  data T a where
>    T1 :: T a
>    T2 :: T Int
>
>  -- Does this typecheck?
>  f :: C a b => T a -> Bool
>  f T1 = True
>  f T2 = op 3
>
> The function f "should" typecheck because inside the T2 branch we know that
> (a~Int), and hence by the fundep (b~Bool).  But we have no formal type
> system for fundeps that describes this, and GHC's implementation certainly
> rejects it.


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
challenges.

Probably, Simon is refrerring to the 'unresolved' issue of providing a
System F style translation for fundeps + local constraints. 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.

-Martin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100701/b3152e5c/attachment.html