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)
My intent is that (:+:) really is injective in each argument (holding the
other as fixed), but I don't know how to pers
Isn't this what data families (as opposed to type families) do?
John
On Mon, Feb 14, 2011 at 1:28 PM, 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
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 wrote:
> Isn't this what data families (as opposed to type families) do?
>
>John
>
> On Mon, Feb 14, 2011 at 1:28 PM, C
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 wrote:
> Yes, it's one things that data families do. Another is introducing *new*
> data types rather than reusing existing ones. - Conal
>
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 co
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
>
> On Mon, Feb 14, 2011 at 1:41 PM, John Meacham wrote:
>
>> Isn't this what data families (as opposed to type families) do?
>
>
On Tue, Feb 15, 2011 at 7:02 AM, Conal Elliott wrote:
> Yes, it's one things that data families do. Another is introducing *new*
> data types rather than reusing exis
u 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
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
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 injectiv
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 :
Haskellers,
I am finishing work on adding injective type families to GHC. I know that in
the past many people
have asked for this feature. If you have use cases for injective type families
I would appreciate
if you could show them to me. My implementation has some restrictions and I
want to
Hi!
Injective type families as supported by GHC 8.0.1 do not behave like I
would expect them to behave from my intuitive understanding.
Let us consider the following example:
> {-# LANGUAGE RankNTypes, TypeFamilyDependencies #-}
>
> class C a where
>
> type T a = b | b -&g
C, GHC's core language, to do so.
Simon
| -Original Message-
| From: Glasgow-haskell-users [mailto:glasgow-haskell-users-
| boun...@haskell.org] On Behalf Of Wolfgang Jeltsch
| Sent: 05 July 2017 01:21
| To: glasgow-haskell-users@haskell.org
| Subject: Trouble with injective ty
t you'd need to extend System FC, GHC's core language, to
> do so.
>
> Simon
>
>
> >
> > -Original Message-
> > From: Glasgow-haskell-users [mailto:glasgow-haskell-users-
> > boun...@haskell.org] On Behalf Of Wolfgang Jeltsch
> > Sent
T Int ~ b). False |> ??
>>
>> Again, what evidence can we use to cast False to 'a'.
>>
>>
>> In short, fundeps and type family dependencies only add extra
>> unification constraints, which may help to resolve ambiguous
>> types. They don’t provide evidenc
;> types. They dont provide evidence. That's not to say
that they
>> couldn't. But you'd need to extend System FC, GHC's core
language, to
>> do so.
>>
>> Simon
>>
>>
>>>
>>> -Original Message-
&
n the draft), if we
treat them as type-level functions. Hence, we had to tighten up the
restrictions imposed on them, good thing that until now they didn't affect
the generated System FC code!
There is still some work to be done to transfer the results to injective
type families but I believ
[(),()]) => Proxy y
Prints
desired :: Proxy '[y, y1]
current :: HLength y ~ 'HSucc ('HSucc 'HZero) => Proxy y
Regards,
Adam
On Mon, Feb 9, 2015 at 10:58 AM, Jan Stolarek wrote:
> Haskellers,
>
> I am finishing work on adding injective type families to GHC. I know
Thank you Adam.
> One example is https://github.com/haskell/vector/issues/34
Yes, this looks like an example where injectivity will work. One question here:
how does one build
vector with GHC HEAD? I tried but failed because of dependencies.
> I see lots of potential uses in HList. For example
On Tue, Feb 10, 2015 at 6:38 AM, Jan Stolarek wrote:
>> I don't know how realistic this is but a constraint (HLength x ~
>> HLength y) would ideally have the same result as SameLength x y.
> I'm not sure if I understand that part. HLength is not injective. How would
> injectivity help here?
I ag
Hello List,
With ghc - 7.8 and 7.6 the following program is accepted:
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
class (UnF (F a) ~ a, Show a) => C a where
type F a
f :: F a -> a
type family UnF a
g :: forall a. C a => a -> String
g _ = show a
where a = f (und
After quite a bit of thought, I agree that this is a regression and that the
original program should be accepted.
Make a bug report!
Thanks,
Richard
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman
I've added it as https://ghc.haskell.org/trac/ghc/ticket/10009
On Tue, Jan 20, 2015 at 11:23 AM, Richard Eisenberg wrote:
> After quite a bit of thought, I agree that this is a regression and that the
> original program should be accepted.
>
> Make a bug report!
>
> Thanks,
> Richard
___
And I've closed it as worksforme. I couldn't reproduce the problem
with 7.11.20150103.
On Tue, Jan 20, 2015 at 11:42 AM, adam vogt wrote:
> I've added it as https://ghc.haskell.org/trac/ghc/ticket/10009
>
> On Tue, Jan 20, 2015 at 11:23 AM, Richard Eisenberg
> wrote:
>> After quite a bit of tho
Wrongly, as it turned out. Sorry! The problem remains.
On Tue, Jan 20, 2015 at 2:37 PM, David Feuer wrote:
> And I've closed it as worksforme. I couldn't reproduce the problem
> with 7.11.20150103.
>
> On Tue, Jan 20, 2015 at 11:42 AM, adam vogt wrote:
>> I've added it as https://ghc.haskell.org
| To: adam vogt
| Cc: Glasgow-Haskell-Users
| Subject: Re: ghc-7.10.0 type inference regression when faking injective
| type families
|
| After quite a bit of thought, I agree that this is a regression and that
| the original program should be accepted.
|
| Make a bug report!
|
| Thanks
26 matches
Mail list logo
