Exposing newtype coercions to Haskell
mail at joachim-breitner.de
Tue Jul 2 16:32:22 CEST 2013
Am Dienstag, den 02.07.2013, 14:11 +0000 schrieb Simon Peyton-Jones:
> I'm not sure that a plugin is the way to go here, though it's a good
as I said, it is just to host the prototype that allows for quick
experimentation and allows people to test it without having to compile
> · I’m not sure how you expect to deal with essential NT
> newtype T a = MkT a a
> tNT :: NT a b -> NT (T a) (T b)
> tNT n = createNT ???
I planned to use
tNT = error "magic message to GHC.NT.Plugin"
that is then replaced by GHC.NT.Plugin (and if for some reason it is
missed by it it stays type safe)
> To your questions:
> · To do these kind of things, CoreM will need more reader stuff.
> In particular:
> o The global TypeEnv
> o The GlobalRdrEnv
Ok, I guess this means that I’ll need to leave the easy land of Plugin
experimentation very soon...
I also noticed a problem with my logic for creating the NT-lifting
function: Just having the constructors of C in scope is not sufficient
to safely provide
NT a b -> NT (C a) (C b)
as the parameters of the constructor might wrap a in another type
data Foo a = Foo (Set a)
then we certainly don’t want the user to be able to write
deriving fooNT :: NT a b -> NT (Foo a) (Foo b)
as he can easily get the unwanted (Set a) -> (Set b) coercion for
arbitrary a b from that. So in this example, the compiler should at most
deriving fooNT :: NT (Set a) (Set b) -> NT (Foo a) (Foo b)
but it feels a bit weird that the „internals“ of Foo are relevant here.
Following this line of thought it means that for
data Proxy a = Proxy
we would allow
deriving proxyNT :: NT (Proxy a) (Proxy b)
without a "NT a b" parameter, as long as the Proxy data constructor is
e-Mail: mail at joachim-breitner.de
Jabber-ID: nomeata at joachim-breitner.de
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Size: 198 bytes
Desc: This is a digitally signed message part
More information about the Glasgow-haskell-users