TypeFamilies vs. FunctionalDependencies & type-level recursion

Simon Peyton-Jones simonpj at microsoft.com
Thu May 24 16:24:45 CEST 2012


See also http://hackage.haskell.org/trac/ghc/wiki/NewAxioms
(as yet unimplemented)

Simon

| -----Original Message-----
| From: haskell-prime-bounces at haskell.org [mailto:haskell-prime-
| bounces at haskell.org] On Behalf Of AntC
| Sent: 24 May 2012 14:00
| To: haskell-prime at haskell.org
| Subject: Re: TypeFamilies vs. FunctionalDependencies & type-level
| recursion
| 
|  <oleg at ...> writes:
| 
| >
| >
| > I don't think Overlapping Instances will be in Haskell' any time soon
| > since there are doubts about the soundness. Overlapping instances are
| > clearly unsound with type functions. Whether they are sound with
| > functional dependencies is not clear, but there are warning
| > signs:
| >
| > 	http://www.haskell.org/pipermail/haskell-cafe/2010-July/080043.html
| >
| I have now worked through that post in detail, thank you. And replied
| (on the cafe http://www.haskell.org/pipermail/haskell-cafe/2012-
| May/101417.html )
| 
| As SPJ says there, I don't expect there's any real difference in the
| fundeps approach compared to type families. And as a matter of taste, I
| find type families more easy to understand and reason about, and more
| *functional*.
| 
| But I don't see in SPJ's post any real doubts about soundness, just
| restrictions that would have to be imposed. He concludes "I believe that
| if ..., then overlap of type families would be fine."
| 
| The only onerous restriction is that overlapping instances would have to
| be in a single module. And I don't think that is needed under my
| proposal to dis- overlap overlaps.
| 
| As a matter of interest, how would the TTypeable approach address those
| examples? Particularly the existentials (examples 3 and 4). How would it
| look inside the GADTs to discharge the constraints (or apply the type
| functions)?
| 
| I notice example 4 (and 1) 'exploits' separate compilation/imported
| overlapping instances to arrive at unsoundness. How does TTypeable
| handle imported instances?
| 
| AntC
| 
| 
| 
| _______________________________________________
| Haskell-prime mailing list
| Haskell-prime at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell-prime





More information about the Haskell-prime mailing list