Injective type families?
Iavor Diatchki
iavor.diatchki at gmail.com
Tue Feb 15 09:52:55 CET 2011
Hello,
shouldn't the check go the other way? (i.e., if the RHSs unify, then the
LHS must be the same). Here is an example:
-- This function is not injective.
type instance F a = Int
type instance F b = Int
Still, Conal's example would not work if we just added support for injective
type functions because + is not injective (e.g., 2 + 3 = 1 + 4). Instead,
what we'd need to say is that it is injective in each argument separately,
which would basically amount to adding functional dependencies to type
functions. Perhaps something like this:
type family (a :+: b) ~ c | c b -> a, c a -> b
This seems like a feature which could be useful.
-Iavor
PS: Conal, I have been working on a GHC extension which has direct support
for working with natural numbers at the type-level (e.g., + is a built-in
type function which supports cancellation and other properties of the normal
+ operation). I am keen on collecting different ways in which people use
type-level naturals to make sure that my implementation supports them (or at
least report a decent error). I wasn't sure if the :+ from your example was
just meant to illustrate the issue with injectivity, but if you have a use
case for type nats, I'd be curious to find out more.
On Mon, Feb 14, 2011 at 3:26 PM, Simon Peyton-Jones
<simonpj at microsoft.com>wrote:
> 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.
>
> Simon
>
> | -----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
> | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20110215/f909a7e0/attachment.htm>
More information about the Glasgow-haskell-users
mailing list