Injective type families?
simonpj at microsoft.com
Tue Feb 15 00:26:26 CET 2011
Injective type families are a perfectly reasonable idea, but we have not implemented them (yet). The idea would be:
* You declare the family to be injective
injective type family T a :: *
* At every type instance, injectivity is checked. That is, if you say
type instance T (a,Int) = Either a Bool
then we must check that every type instance whose LHS unifies with this has the same RHS under the unifying substitution. Thus
type instance T (a,Bool) = [a] -- OK; does not unify
type instance T (Int,b) = Either Int Bool -- OK; same RHS on (Int,Int)
I think it's mainly a question of tiresome design questions (notably do we want a new keyword "injective"? Should it go before "type"?) and hacking to get it all implemented.
| -----Original Message-----
| From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-users-
| bounces at haskell.org] On Behalf Of Dan Doel
| Sent: 14 February 2011 23:14
| To: glasgow-haskell-users at haskell.org
| Subject: Re: Injective type families?
| On Monday 14 February 2011 5:51:55 PM Daniel Peebles wrote:
| > I think what you want is closed type families, as do I and many others :)
| > Unfortunately we don't have those.
| Closed type families wouldn't necessarily be injective, either. What he wants
| is the facility to prove (or assert) to the compiler that a particualr type
| family is in fact injective.
| It's something that I haven't really even seen developed much in fancy
| dependently typed languages, though I've seen the idea before. That is: prove
| things about your program and have the compiler take advantage of it.
| -- Dan
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users at haskell.org
More information about the Glasgow-haskell-users