On 14/02/2011, at 21:28, Conal Elliott wrote:
Is there a way to declare a type family to be injective?
I have
data Z
data S n
type family n :+: m
type instance Z :+: m = m
type instance S n :+: m = S (n :+: m)
You could prove it :-)
class Nat n where
induct :: p Z -
Message-
| From: glasgow-haskell-users-boun...@haskell.org [mailto:
glasgow-haskell-users-
| boun...@haskell.org] On Behalf Of Dan Doel
| Sent: 14 February 2011 23:14
| To: glasgow-haskell-users@haskell.org
| Subject: Re: Injective type families?
|
| On Monday 14 February 2011 5:51:55
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
Yes, you’re right.
Still, Conal's example would not work if we just added support for
Isn't this what data families (as opposed to type families) do?
John
On Mon, Feb 14, 2011 at 1:28 PM, Conal Elliott co...@conal.net wrote:
Is there a way to declare a type family to be injective?
I have
data Z
data S n
type family n :+: m
type instance Z :+: m = m
type instance S
Yes, it's one things that data families do. Another is introducing *new*
data types rather than reusing existing ones. - Conal
On Mon, Feb 14, 2011 at 1:41 PM, John Meacham j...@repetae.net wrote:
Isn't this what data families (as opposed to type families) do?
John
On Mon, Feb 14, 2011
I think what you want is closed type families, as do I and many others :)
Unfortunately we don't have those.
On Mon, Feb 14, 2011 at 10:02 PM, Conal Elliott co...@conal.net wrote:
Yes, it's one things that data families do. Another is introducing *new*
data types rather than reusing existing
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
Of Dan Doel
| Sent: 14 February 2011 23:14
| To: glasgow-haskell-users@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
On Mon, Feb 14, 2011 at 1:41 PM, John Meacham j...@repetae.net wrote:
Isn't this what data families (as opposed to type families) do?
On Tue, Feb 15, 2011 at 7:02 AM, Conal Elliott co...@conal.net wrote:
Yes, it's one things that data families do. Another is introducing *new*
data types
