Hi Joachim,
As discussed previously, I do think we need a way to store representational
coercions. In my roles branch (which is getting close to pushing, I believe), I
have created eqReprPrimTyCon, which is like eqPrimTyCon, but it is the type of
coercions witnessing representational equality.
Hi,
Am Dienstag, den 23.07.2013, 18:58 + schrieb Simon Peyton-Jones:
> If you add -XIncoherentInstances *just to the module that has instance
> IsNT a a*, then it'll work fine I think. This says "pick this
> instance even though an instantiation of the constraint might match a
> more specific
du]
| Sent: 23 July 2013 23:12
| To: Simon Peyton-Jones
| Cc: Joachim Breitner; ghc-devs@haskell.org
| Subject: Re: Exposing newtype coercions to Haskell
|
| Yes, that's what I got from Joachim's response to my design, also. My only
other
| thought is to have some way to sto
Behalf Of Richard
> | Eisenberg
> | Sent: 23 July 2013 09:51
> | To: Joachim Breitner
> | Cc: ghc-devs@haskell.org
> | Subject: Re: Exposing newtype coercions to Haskell
> |
> | A few responses:
> |
> | - As Simon said, there is no great reason we don't have ~
ghc-devs [mailto:ghc-devs-boun...@haskell.org] On Behalf Of Joachim
| Breitner
| Sent: 23 July 2013 12:45
| To: ghc-devs@haskell.org
| Subject: Re: Exposing newtype coercions to Haskell
|
| Hi,
|
| Am Dienstag, den 23.07.2013, 09:51 +0100 schrieb Richard Eisenberg:
| > I think that thi
| Eisenberg
| Sent: 23 July 2013 09:51
| To: Joachim Breitner
| Cc: ghc-devs@haskell.org
| Subject: Re: Exposing newtype coercions to Haskell
|
| A few responses:
|
| - As Simon said, there is no great reason we don't have ~R# in Core.
| It's just that we looked through G
Hi,
Am Dienstag, den 23.07.2013, 09:51 +0100 schrieb Richard Eisenberg:
> I think that thinking about the base case is also
> productive, but I don't have a clear enough opinion to express on that
> front.
and it seems to tricky; Here we are hitting problems that we did not
have with the non-cla
You're right, of course. I'm now thinking we really do need ~R# to make
this work. That's annoying, but not technically difficult. I'll continue
to think about this.
Richard
On 2013-07-23 10:00, Joachim Breitner wrote:
Hi,
Am Dienstag, den 23.07.2013, 09:51 +0100 schrieb Richard Eisenberg:
Hi,
Am Dienstag, den 23.07.2013, 09:51 +0100 schrieb Richard Eisenberg:
> A few responses:
>
> - As Simon said, there is no great reason we don't have ~R# in Core.
> It's just that we looked through GHC and, without newtype coercions,
> there is no need for ~R#, so we opted not to include it. I
A few responses:
- As Simon said, there is no great reason we don't have ~R# in Core.
It's just that we looked through GHC and, without newtype coercions,
there is no need for ~R#, so we opted not to include it. I'm still not
convinced we need it for newtype coercions, though. What if we have
Hi Richard and Simon,
thanks for your detailed notes.
Am Montag, den 22.07.2013, 17:01 +0100 schrieb Richard Eisenberg:
> - I think you *do* want HsExprs not CoreExprs. Though I haven't worked
> much in TcDeriv myself, I imagine everything uses HsExprs so that they
> can be type-checked. This
| - But, there's a wrinkle here. The (~#) type, along with (~) and (:=:)
| (the last is from the soon-to-be Data.Type.Equality), all work over
| so-called *nominal* coercions. (Nominal coercions correspond to the "C"
| coercions from this paper:
Excellent point, Richard.
Running example
Hi Joachim,
A few responses to your plan:
- I think you *do* want HsExprs not CoreExprs. Though I haven't worked
much in TcDeriv myself, I imagine everything uses HsExprs so that they
can be type-checked. This allows nice error messages to be reported at
the site of a user's "deriving instanc
Hi,
as discussed, I started to work basing the newtype coercions on classes
instead of types. I poked around the code, especially TcDeriv.lhs, and I
have a few questions:
For my current design I wanted to have
class IsNT a where
type Concrete a
coercion ::
It's available here (for now).
http://ittc.ku.edu/~nfrisby/tcrn-plugin.tar.gz
Sorry for the whack build/test infrastructure: I wasn't planning sharing
this write-once experimental code.
The 'MyTcRnDriver.initTcFromModGuts` function and the
'TcRnPlugin.append_guts` are the key functions.
The r
Hi,
Am Dienstag, den 16.07.2013, 07:54 + schrieb Simon Peyton-Jones:
> | I guess it doesn’t change the implementation a lot
>
> Oh I think it does change it a LOT. No more hunting through all the
> in-scope identifier for ones whose type finish with " -> NT t1
> t2". No new syntax. No n
| Are you saying that seq is nonsense? Or that are you just telling me why
| we need seq?
No, no, just that all those seqs are big nuisance -- and one caused solely by
the fact that users could (in effect) write bogus instances. If they can't, the
issue doesn't arise.
| We’ve discussed this pro
Hi,
Am Montag, den 15.07.2013, 21:57 + schrieb Simon Peyton-Jones:
> · note that the “seq” nonsense is because we allow user-defined
> NT-values
Are you saying that seq is nonsense? Or that are you just telling me why
we need seq?
> · also note that to determine which NT values w
-boun...@haskell.org] On
| Behalf Of Joachim Breitner
| Sent: 11 July 2013 09:41
| To: ghc-devs@haskell.org
| Subject: Re: Exposing newtype coercions to Haskell
|
| Hi,
|
| Am Montag, den 08.07.2013, 09:39 + schrieb Simon Peyton-Jones:
| > | > If you CAN do that, then it
POPLing today. Let's discuss on Monday
| -Original Message-
| From: ghc-devs-boun...@haskell.org [mailto:ghc-devs-boun...@haskell.org]
| On Behalf Of Joachim Breitner
| Sent: 11 July 2013 15:25
| To: ghc-devs@haskell.org
| Subject: Re: Exposing newtype coercions to Haskell
|
Hi,
despite my issues with recursive data types, I continued with the
implementation.
I now added the check if the data type arguments can safely be coerced.
I do not scan what is in scope for NT values to use, but rather expect
the progammer to promise the required witness when he uses "deriving
Hi,
Am Montag, den 08.07.2013, 09:39 + schrieb Simon Peyton-Jones:
> | > If you CAN do that, then it's ok (internally) to use ordinary coercion
> | > lifting, roughly
> | > ntT g = T g refl
> | > The above per-constructor-arg testing is just to make sure that all
> | > the relevant witnesses
| > If you CAN do that, then it's ok (internally) to use ordinary coercion
| > lifting, roughly
| > ntT g = T g refl
| > The above per-constructor-arg testing is just to make sure that all
| > the relevant witnesses are in scope, to preserve abstraction. It's
| > not for soundness.
|
| I unde
Hi,
Am Freitag, den 05.07.2013, 08:10 + schrieb Simon Peyton-Jones:
> Re passing bottoms, read "Equality proofs and deferred type errors".
> http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/
> The NT type here is playing the role of (~) in that paper. Just as (~)
> wraps (~#)
lasgow-haskell-
| users-boun...@haskell.org] On Behalf Of Joachim Breitner
| Sent: 04 July 2013 14:30
| To: glasgow-haskell-us...@haskell.org
| Subject: Re: Exposing newtype coercions to Haskell
|
| Hi,
|
| small update: I generalized the code at
| https://github.com/nomeata/nt-coerce/blob/9349dd3
25 matches
Mail list logo
