Joachim Breitner | 1 Jul 13:59 2013
Picon

Exposing newtype coercions to Haskell

Hi,

this is related to
http://hackage.haskell.org/trac/ghc/wiki/NewtypeWrappers#Proposal3.
I tried to hack up a little prototype of this, and this “works” now:

        import GHC.NT

        newtype Age = Age Int deriving Show

        ageNT :: NT Age Int
        ageNT = createNT

        newtype MyList a = MyList [a] deriving Show

        myListNT :: NT (MyList a) [a]
        myListNT = createNT

        
        main = do
            let n = 1 :: Int
            let a = coerce (sym ageNT) 1
            let l1 = [a]
            let l2 = coerce (listNT ageNT) l1
            let l3 = coerce (sym myListNT) l2
            print a
            print l2
            print l3

will print
(Continue reading)

Simon Peyton-Jones | 2 Jul 16:11 2013
Picon

RE: Exposing newtype coercions to Haskell

Good stuff.  The basic idea seems good to me.

 

I'm not sure that a plugin is the way to go here, though it's a good start. 

·        Exactly which programs are type-correct?  Eg
    coerce (listNT createNT)

It all depends on exactly what type args createNT is applied to.

·        A function f = createNT probably would not be accepted.  But if ‘f’ was inlined sufficiently early (before the plugin) it might.

·        Giving an error message in terms of exactly the text the user wrote is harder.

·        I’m not sure how you expect to deal with essential NT arguments:

newtype T a = MkT a a

tNT :: NT a b -> NT (T a) (T b)

tNT n = createNT ???

 

On the whole I think a ‘deriving’ form would be preferable.  And then yes, you’ll need to build HEAD.

 

To your questions:

·        To do these kind of things, CoreM will need more reader stuff.  In particular:

o   The global TypeEnv

o   The GlobalRdrEnv

·        I don’t think we have generic Core traversal functions, perhaps because almost every such pass needs to deal with binders.

 

Simon

 

 

-----Original Message-----

From: glasgow-haskell-users-bounces <at> haskell.org [mailto:glasgow-haskell-users-

bounces <at> haskell.org] On Behalf Of Joachim Breitner

Sent: 01 July 2013 13:00

To: glasgow-haskell-users <at> haskell.org

Subject: Exposing newtype coercions to Haskell

|  Hi,

|  this is related to

|  http://hackage.haskell.org/trac/ghc/wiki/NewtypeWrappers#Proposal3.

|  I tried to hack up a little prototype of this, and this “works” now:

|          import GHC.NT

|          newtype Age = Age Int deriving Show

|          ageNT :: NT Age Int

|          ageNT = createNT

|          newtype MyList a = MyList [a] deriving Show

|          myListNT :: NT (MyList a) [a]

|          myListNT = createNT

|          main = do

|              let n = 1 :: Int

|              let a = coerce (sym ageNT) 1

|              let l1 = [a]

|              let l2 = coerce (listNT ageNT) l1

|              let l3 = coerce (sym myListNT) l2

|              print a

|              print l2

|              print l3

|  will print

|          Age 1

|          [1]

|          MyList [1]

|  and no unsafeCoerce and no map is used in the production of this output.

|  The GHC.NT module provides:

|  data NT a b

|  coerce :: NT a b -> a -> b

|  refl   :: NT a a

|  sym    :: NT a b -> NT b a

|  trans  :: NT a b -> NT b c -> NT a c

|  createNT :: NT a b

|  listNT :: NT a b -> NT [a] [b]

|  where createNT takes the place of the "deriving foo :: NT a b" syntax:

|  At compile time, it is checked if its first type argument is a newtype of the second,

|  and the corresponding coercion is inserted, otherwise an error is (well, will be)

|  printed.

|  The idea is that these coercions will be guaranteed to be free (or almost free; I am

|  not sure if the coercion witness (NT a b) will actually be optimized away).

|  The prototype can be found at

|  https://github.com/nomeata/nt-coerce

|  and is implemented as a GHC plugin compatible with GHC 7.6.3 (I chose this

|  route as it means not having to compile GHC). You can check if it works for you via

|  $ ghc  -dcore-lint -package ghc --make test.hs  && ./test

|  The code itself is, well, at most prototype code quality and contains quite a

|  number of hacks and other warts, mostly due to my inexperience with GHC

|  hacking, and I could make use of some advice. Some more concrete questions:

|   * How do I look up a module (here GHC.NT.Type) and a name therein (NT) in

|  CoreM? I tried to go via getOrigNameCache, but passing the ModuleName name to

|  lookupModuleEnv yielded Nothing, although it seems to me to be precisely the

|  same name that I find in moduleEnvKeys. If I take the ModuleName from that list,

|  it works. Similar problems with the OccEnv.

|  Please see

|  https://github.com/nomeata/nt-

|  coerce/blob/edef9f4d4889dde651bb086e76c576f84e8f8aec/GHC/NT/Plugin.hs#L9

|  9

|  for what I tried (and how I worked around it). This work-around also prevents

|  building the package with cabal right now.

|   * I did not find generic Core traversal functions like traverse :: (Monad m) =>

|  (Expr a -> m (Maybe (Expr a))) -> Expr a -> m (Expr a) which  I defined in

|  https://github.com/nomeata/nt-

|  coerce/blob/edef9f4d4889dde651bb086e76c576f84e8f8aec/GHC/NT/Plugin.hs#L2

|  31.

|  Are such traversals re-implemented everywhere or did I just not search well

|  enough?

|   * On the core level, once I have a TyCon, I also have all DataCons available. Is

|  there already code present that checks if the currently compiled module really

|  should see the data constructors, i.e. if they are exported? I see code in

|  normaliseFfiType, but that seems to be integrated in the type checker, and it

|  seems I need a GlobalRdrEnv; can I get such a thing in a Core2Core pass?

|  Thanks,

|  Joachim

|  --

|  Joachim “nomeata” Breitner

|    mail <at> joachim-breitner.de • http://www.joachim-breitner.de/

|    Jabber: nomeata <at> joachim-breitner.de  • GPG-Key: 0x4743206C

|    Debian Developer: nomeata <at> debian.org

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Joachim Breitner | 2 Jul 16:32 2013
Picon

Re: Exposing newtype coercions to Haskell

Hi,

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
> start.  

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
GHC.

> ·       I’m not sure how you expect to deal with essential NT
> arguments:
> 
> 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
constructor, i.e.

        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
accept

        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
in scope. 

Greetings,
Joachim
--

-- 
Joachim Breitner
  e-Mail: mail <at> joachim-breitner.de
  Homepage: http://www.joachim-breitner.de
  ICQ#: 74513189
  Jabber-ID: nomeata <at> joachim-breitner.de
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon Peyton-Jones | 2 Jul 18:28 2013
Picon

RE: Exposing newtype coercions to Haskell


| I also noticed a problem with my logic for creating the NT-lifting
| function.  Suppose
|   data C a = MkC (Foo a)
| 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
| constructor, eg
|         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)

Dually, suppose Foo was an *abstract* type, where we can't see the constructors of Foo.  But the programmer
as exported fooNT :: NT a b -> NT (Foo a) (Foo b).  Then we *do* want to be able to derive
	cNT :: NT a b -> NT (C a) (C b)
Instead maybe we say
	deriving cNT :: NT a b -> NT (C a) (C b) using( fooNT )
listing the imported witnesses that we use.  Or maybe we say simply
	deriving cNT :: NT a b -> NT (C a) (C b) 
and magically use any NT-typed things that are in scope.

This clearly deserves treatment on the wiki page.

The criterion "could you write it by hand?" remains a good one.

Simon
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Joachim Breitner | 3 Jul 10:01 2013
Picon

Re: Exposing newtype coercions to Haskell

Hi,

Am Dienstag, den 02.07.2013, 16:28 +0000 schrieb Simon Peyton-Jones:
> | I also noticed a problem with my logic for creating the NT-lifting
> | function.  Suppose
> |   data C a = MkC (Foo a)
> | 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
> | constructor, eg
> |         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)
> 
> Dually, suppose Foo was an *abstract* type, where we can't see the constructors of Foo.  But the programmer
as exported fooNT :: NT a b -> NT (Foo a) (Foo b).  Then we *do* want to be able to derive
> 	cNT :: NT a b -> NT (C a) (C b)
> Instead maybe we say
> 	deriving cNT :: NT a b -> NT (C a) (C b) using( fooNT )
> listing the imported witnesses that we use.  Or maybe we say simply
> 	deriving cNT :: NT a b -> NT (C a) (C b) 
> and magically use any NT-typed things that are in scope.

Is this really the compiler’s job here? After all, the programmer would
be able to write

        deriving cNT' :: NT (Foo a) (Foo b) -> NT (C a) (C b)
        cNT :: NT a b -> NT (C a) (C b)
        cNT = cNT' . fooNT

and expose just cNT to his users, so no expressiveness is lost by not
providing automatic support here.

> This clearly deserves treatment on the wiki page.

Added.

> The criterion "could you write it by hand?" remains a good one.

Agreed.

Greetings,
Joachim

--

-- 
Joachim “nomeata” Breitner
  mail <at> joachim-breitner.de • http://www.joachim-breitner.de/
  Jabber: nomeata <at> joachim-breitner.de  • GPG-Key: 0x4743206C
  Debian Developer: nomeata <at> debian.org
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon Peyton-Jones | 3 Jul 21:40 2013
Picon

RE: Exposing newtype coercions to Haskell

|  Is this really the compiler’s job here? After all, the programmer would be able to
|  write
|  
|          deriving cNT' :: NT (Foo a) (Foo b) -> NT (C a) (C b)
|          cNT :: NT a b -> NT (C a) (C b)
|          cNT = cNT' . fooNT
|  
|  and expose just cNT to his users, so no expressiveness is lost by not providing
|  automatic support here.

True.  But it could get pretty inconvenient.

	data Foo a = F1 [a] (Tree [a]) (Maybe a) [Maybe a]

We could restrict you (only ) to saying

	deriving fooNT
		:: NT [a] [b]
 		-> NT (Tree [a]) (Tree [b]) 
		-> NT (Maybe a) (Maybe b)
		-> NT [Maybe a] [Maybe b]
		-> NT (Foo a) (Foo b)

but the excitement would wear off pretty fast :-).   It'd be nicer to write
	deriving fooNT :: NT a b -> NT (Foo a) (Foo b)
and  have the compiler use the other lexically-in-scope NT values to solve the problem.  This is, after all,
precisely what the type-class inference machinery does.

There's something a bit strange about looking for all NT values that are lexically in scope; it all amounts
to something pretty similar to named type-class instances.

Simon


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Joachim Breitner | 4 Jul 15:30 2013
Picon

Re: Exposing newtype coercions to Haskell

Hi,

small update: I generalized the code at
https://github.com/nomeata/nt-coerce/blob/9349dd3/GHC/NT/Plugin.hs
a bit, it is now able to handle to create NT-values for unwarpping
arbitrary newtypes and for lifting across type constructors. It does so
unconditionally, i.e. does _not_ yet check whether the constructors are
in scope and whether the user is allowed to cast the types occurring in
the data constructors.

So what works is this:

NT values for newtypes without or with type arguments, and possibly
recursive:

        newtype Age = Age Int deriving Show
        ageNT :: NT Age Int
        ageNT = deriveThisNT   -- temporary syntax for deriving
        listNT ...

        newtype MyList a = MyList [a] deriving Show
        myListNT :: NT (MyList a) [a]
        myListNT = deriveThisNT

        newtype R a = R [R a] deriving Show
        rNT :: NT (R a) [R a]
        rNT = deriveThisNT

NT values for type constructors, replacinge all or some of the type
parameters:

        listNT :: NT a b -> NT [a] [b]
        listNT = deriveThisNT    

        myListNT' :: NT a b -> NT (MyList a) (MyList b)
        myListNT' = deriveThisNT

        data F a b c = F a b c deriving Show
        fNT :: NT a a' -> NT (F a b c) (F a' b c)
        fNT = deriveThisNT

What does not work is creating a NT value between a newtype and its
representation if type arguments change on the way, e.g.

        bar :: NT (MyList Age) [Int]

but the user can construct that himself:

        bar = myListNT' ageNT `trans` myListNT

The next step would be to add the safeguards about the visibility of
constructors and about the types of data constructor parameters.
Especially the latter is still not clear to me: For example with

        data Foo a = Foo (Bar a)

is it really sufficient to check whether a "barNT:: NT a b -> NT (Bar a)
(Bar b)" exists? After all, I would not need barNT in the generated
implementation of fooNT, so the user could “provide” this value via
undefined and nobody would notice.

I get the feeling that already the typing rule for TyConAppCo should
expect coercions between the actual types in the data constructors
rather than just between the type constructor parameters, so that the
implementation barNT would actually have to use fooNT. Maybe that would
simplify the two-equalities-approach. But that is just an uneducated gut
feeling.

BTW: Is this still on-topic on glasgow-haskell-users or should I move to
ghc-dev?

Greetings,
Joachim
--

-- 
Joachim “nomeata” Breitner
  mail <at> joachim-breitner.de • http://www.joachim-breitner.de/
  Jabber: nomeata <at> joachim-breitner.de  • GPG-Key: 0x4743206C
  Debian Developer: nomeata <at> debian.org
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon Peyton-Jones | 5 Jul 10:10 2013
Picon

RE: Exposing newtype coercions to Haskell

(Narrowing to ghc-devs.)

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 (~#), so NT will wrap (NT#), and
it'll play out exactly in the paper.  So I'm not bothered about bottoms.

Suppose we have a data type 
	data T a b = T1 (S a b) (R b)
where we have in scope
	ntS :: NT p p' -> NT q q' -> NT (S p q) (S p' q')
but R is completely abstract.  Now, is it safe to say

	deriving ntT :: NT a a' -> NT (T a b) (T a' b)

Well, our criterion is whether we can write by hand, a function
	foo :: NT a a' -> T a b -> T a' b

Let's try:
	foo g (T1 s r) = T1 (cast s g1) (cast r g2)
          where
            g1 :: NT (S a b) (S a' b)
		g1 = ntS g refl

		g2 :: NT (R b) (R b)
		g2 = refl

So the general plan is, for each constructor argument of type ty, see if you can build a suitable NT value (g1,
g2 in the above example), using either built-in stuff like refl, or arguments like (g :: NT a a'), or
in-scope NT values like ntS.

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.

(There is some "role" stuff to take account of there, which Richard is working on, but to a first
approximation that's it I think.)

Simon

| -----Original Message-----
| From: glasgow-haskell-users-bounces <at> haskell.org [mailto:glasgow-haskell-
| users-bounces <at> haskell.org] On Behalf Of Joachim Breitner
| Sent: 04 July 2013 14:30
| To: glasgow-haskell-users <at> 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/GHC/NT/Plugin.hs

| a bit, it is now able to handle to create NT-values for unwarpping
| arbitrary newtypes and for lifting across type constructors. It does so
| unconditionally, i.e. does _not_ yet check whether the constructors are
| in scope and whether the user is allowed to cast the types occurring in
| the data constructors.
| 
| So what works is this:
| 
| NT values for newtypes without or with type arguments, and possibly
| recursive:
| 
|         newtype Age = Age Int deriving Show
|         ageNT :: NT Age Int
|         ageNT = deriveThisNT   -- temporary syntax for deriving
|         listNT ...
| 
|         newtype MyList a = MyList [a] deriving Show
|         myListNT :: NT (MyList a) [a]
|         myListNT = deriveThisNT
| 
|         newtype R a = R [R a] deriving Show
|         rNT :: NT (R a) [R a]
|         rNT = deriveThisNT
| 
| 
| NT values for type constructors, replacinge all or some of the type
| parameters:
| 
|         listNT :: NT a b -> NT [a] [b]
|         listNT = deriveThisNT
| 
|         myListNT' :: NT a b -> NT (MyList a) (MyList b)
|         myListNT' = deriveThisNT
| 
|         data F a b c = F a b c deriving Show
|         fNT :: NT a a' -> NT (F a b c) (F a' b c)
|         fNT = deriveThisNT
| 
| 
| What does not work is creating a NT value between a newtype and its
| representation if type arguments change on the way, e.g.
| 
|         bar :: NT (MyList Age) [Int]
| 
| but the user can construct that himself:
| 
|         bar = myListNT' ageNT `trans` myListNT
| 
| 
| 
| The next step would be to add the safeguards about the visibility of
| constructors and about the types of data constructor parameters.
| Especially the latter is still not clear to me: For example with
| 
|         data Foo a = Foo (Bar a)
| 
| is it really sufficient to check whether a "barNT:: NT a b -> NT (Bar a)
| (Bar b)" exists? After all, I would not need barNT in the generated
| implementation of fooNT, so the user could “provide” this value via
| undefined and nobody would notice.
| 
| I get the feeling that already the typing rule for TyConAppCo should
| expect coercions between the actual types in the data constructors
| rather than just between the type constructor parameters, so that the
| implementation barNT would actually have to use fooNT. Maybe that would
| simplify the two-equalities-approach. But that is just an uneducated gut
| feeling.
| 
| 
| BTW: Is this still on-topic on glasgow-haskell-users or should I move to
| ghc-dev?
| 
| 
| Greetings,
| Joachim
| --
| Joachim “nomeata” Breitner
|   mail <at> joachim-breitner.de • http://www.joachim-breitner.de/

|   Jabber: nomeata <at> joachim-breitner.de  • GPG-Key: 0x4743206C
|   Debian Developer: nomeata <at> debian.org
_______________________________________________
ghc-devs mailing list
ghc-devs <at> haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs
Joachim Breitner | 7 Jul 13:28 2013
Picon

Re: Exposing newtype coercions to Haskell

Hi,

Am Freitag, den 05.07.2013, 08:10 +0000 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 (~#), so NT will wrap (NT#), and it'll play out exactly in the
> paper.  So I'm not bothered about bottoms.

I still am. Let’s have a look at your example:

> Suppose we have a data type 
> 	data T a b = T1 (S a b) (R b)
> where we have in scope
> 	ntS :: NT p p' -> NT q q' -> NT (S p q) (S p' q')
> but R is completely abstract.  Now, is it safe to say
> 	deriving ntT :: NT a a' -> NT (T a b) (T a' b)
> 
> Well, our criterion is whether we can write by hand, a function
> 	foo :: NT a a' -> T a b -> T a' b
> 
> Let's try:
> 	foo g (T1 s r) = T1 (cast s g1) (cast r g2)
>           where
>             g1 :: NT (S a b) (S a' b)
>             g1 = ntS g refl
> 
> 	    g2 :: NT (R b) (R b)
> 	    g2 = refl
> 
> So the general plan is, for each constructor argument of type ty, see
> if you can build a suitable NT value (g1, g2 in the above example),
> using either built-in stuff like refl, or arguments like (g :: NT a
> a'), or in-scope NT values like ntS.
> 
> 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 understand the approach, but I think it is insufficient. Assume that
the user wants to cheat for some reason and has this definition for ntS,
clearly writable without having access to S’s internals:

ntS :: NT p p' -> NT q q' -> NT (S p q) (S p' q')
ntS _ _ = error "nah nah"

Then the above check succeeds: You can write the function foo, it would
type check and would, at runtime, throw an exception. But the deriving
mechanism can’t predict that, so it would generate the code "ntT g = T g
refl" _which does not use ntS at all_, suddenly allowing a coecion that
breaks the abstraction.

From what I can tell it works in "Equality proofs and deferred type
errors" because the ~ values are actually used (pattern-matched) in the
Core code and bottoms cause the program to fail at the right points.

Hence my gut feeling that there is something fishy about the existing
coercion rule

         a ~/C a'   b ~/C' b'
         –––––––––––––––––––––
         (T a b) ~/C (T a' b')

(which is probably fine for ~/T – I’m currently focusing on the “types
have same representation equality ~/C”) instead of the more
construction-guided rule

     S a b ~/C S a' b'   R b ~/C' R b'
     –––––––––––––––––––––––––––––––––
            (T a b) ~/C (T a' b')

which would ensure that I’d have to actually call ntS and pattern match
the resulting ntS call in the deriving code for ntT, avoiding the
problem shown above.

Maybe (without claiming that I understand the problem fully) these
coercion rules would make the role system obsolete? These problems occur
with GADTs and type families, right? An example for the former would be

        data G a where ABool :: G Bool

for which "a ~/C b -> G a ~/C G b" is not ok. But this data type
declaration becomes, in Core, simply

        data G a where ABool :: a ~/T Bool -> G a

and by the datatype coercion schema hinted at above the rule would
become

        (a ~/T Bool) ~/C (b ~/T Bool) -> G a ~/C G b.

Assuming there is no way to do a ~/C coercion between ~/T witnesses the
bad coercion would be prevented. Refl could still be used there if G has
multiple type parameters and others are ok to coerce.

Similar for type families: A type family "F a" in a data constructor
parameter causes a "F a ~/C F b" requirement to appear which would then
prevent the bad coercion, or restrict it to cases where "F a" and "F b"
indeed to have the same representation.

Greetings,
Joachim

--

-- 
Joachim “nomeata” Breitner
  mail@...http://www.joachim-breitner.de/
  Jabber: nomeata@...  • GPG-Key: 0x4743206C
  Debian Developer: nomeata@...
_______________________________________________
ghc-devs mailing list
ghc-devs@...
http://www.haskell.org/mailman/listinfo/ghc-devs
Simon Peyton-Jones | 8 Jul 11:39 2013
Picon

RE: Exposing newtype coercions to Haskell

| > 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 understand the approach, but I think it is insufficient. Assume that
| the user wants to cheat for some reason and has this definition for ntS,
| clearly writable without having access to S’s internals:
| 
| ntS :: NT p p' -> NT q q' -> NT (S p q) (S p' q')
| ntS _ _ = error "nah nah"

Quite right!  My mistake was to say "if you CAN do that..." and then discard the evidence that you can do it. 
What I should have said is

	* prove a large bunch of NT constraints (one per constructor field)
	* then `seq` them 
	* before returning the "ordinary coercion lifting" result.

The thing is, that the "ordinary coercion lifting" is sound (roles permitting -- should check that right
off the bat).  But we are making a stronger check here, namely that the programmer has exported enough
evidence, to expose abstractions.

Simon


_______________________________________________
ghc-devs mailing list
ghc-devs <at> haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs
Joachim Breitner | 11 Jul 10:41 2013
Picon

Re: Exposing newtype coercions to Haskell

Hi,

Am Montag, den 08.07.2013, 09:39 +0000 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 are in scope, to preserve abstraction.  It's
> | > not for soundness.
> | 
> | I understand the approach, but I think it is insufficient. Assume that
> | the user wants to cheat for some reason and has this definition for ntS,
> | clearly writable without having access to S’s internals:
> | 
> | ntS :: NT p p' -> NT q q' -> NT (S p q) (S p' q')
> | ntS _ _ = error "nah nah"
> 
> Quite right!  My mistake was to say "if you CAN do that..." and then
> discard the evidence that you can do it.  What I should have said is
> 
> 	* prove a large bunch of NT constraints (one per constructor
>           field)
> 	* then `seq` them 
> 	* before returning the "ordinary coercion lifting" result.
> 
> The thing is, that the "ordinary coercion lifting" is sound (roles
> permitting -- should check that right off the bat).  But we are making
> a stronger check here, namely that the programmer has exported enough
> evidence, to expose abstractions.

Although it feels a bit weird to force one set of coercion witnesses
(based on datacon field types) and then use another (based on typecon
parameters), it could have worked, so I did more work in that direction,
but I have hit another obstacle:

Just to clarify that we talk about the same things, an easy case:
        data Family a = Family a a (List a)
        deriving familyNT :: NT a b -> NT (Family a) (Family b)
with "listNT :: NT a b -> NT (List a) (List b)" in scope would get this
implementation:
        familyNT nt = nt `seq` nt `seq` listNT nt `seq`
                      case nt of (NT co -> NT (Family co))
This does ensure that, without breaking abstractions, the user is
allowed to convert the arguments of the datacon and produces a sound
coercion in in the F_C sense.

But what about a simple tree type?
        data Tree a = Tree a (List (Tree a))
        deriving treeNT :: NT a b -> NT (Tree a) (Tree b)
I need to force witnesses for
      * (NT a b) (easy, that is the first argument) and for
      * (NT (List (Tree a)) (NT (List (Tree b)).
        The only way to obtain such a witness is to use listNT, which
        would strictly(!) expect a value of type NT (Tree a) (Tree b),
        which is what I am trying to produce at the moment, so I cannot
        simply call treeNT.

In this case I can work around it by first creating the final NT value
and then use it to create and seq the witnesses required, before
returning the result:
        treeNT nt = let resNT = case nt of (NT co -> NT (Tree co))
                    in nt `seq` listNT resNT `seq` resNT
but this is becoming more and more hacky and inelegant. For example,
with mutually recursive data types, I’d have to detect that they are
mutually recursive and create similar witnesses in advance for all
involved types; for nested recursion I’d have to create multiple
witnesses, and who knows what else can happen.

From a logical point of view, I’d expect the coercion lifting for a
recursive data type to have a type like
        a ~/C b -> (forall ta tb. (ta ~/C tb -> List ta ~/C List tb)) -> Tree a ~/C Tree b
(justified by writing the data type as a fixed point and thinking about
fixed-point induction), but its soundness breaks down immediately as the
function type -> in the second argument is not total.

That’s it for now,
Joachim

--

-- 
Joachim “nomeata” Breitner
  mail@...http://www.joachim-breitner.de/
  Jabber: nomeata@...  • GPG-Key: 0x4743206C
  Debian Developer: nomeata@...
_______________________________________________
ghc-devs mailing list
ghc-devs@...
http://www.haskell.org/mailman/listinfo/ghc-devs
Joachim Breitner | 11 Jul 16:24 2013
Picon

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"
and the plug the functions together by himself:
https://github.com/nomeata/nt-coerce/blob/ec9b5/tests/LiftAbstract.hs

I also added a test suite to show what works already:
https://github.com/nomeata/nt-coerce/tree/master/tests
what does rightfully not work, due to abstraction:
https://github.com/nomeata/nt-coerce/tree/master/tests/failing
and what does not yet work, although it conceivably should:
https://github.com/nomeata/nt-coerce/tree/master/tests/todo

The test suite contains expected output in *.out and *.err, so you can
check out what happens without having to run it. The error messages are
not yet as nice as they should be.

How to proceed from here Is this approach and design good enough to to
into GHC, despite not being able to handle _all_ cases where it
conceivably could, and the slight unwieldiness when coerctions for data
types based on abstract data types?

BTW, I find it quite nice to be able to develop such a feature without
touching GHC’s source. If that is possible for more contributions, the
entry barrier to GHC would be noticeably lowered.

Thanks,
Joachim

--

-- 
Joachim “nomeata” Breitner
  mail@...http://www.joachim-breitner.de/
  Jabber: nomeata@...  • GPG-Key: 0x4743206C
  Debian Developer: nomeata@...
_______________________________________________
ghc-devs mailing list
ghc-devs@...
http://www.haskell.org/mailman/listinfo/ghc-devs
Simon Peyton-Jones | 12 Jul 10:53 2013
Picon

RE: Exposing newtype coercions to Haskell

POPLing today.  Let's discuss on Monday

| -----Original Message-----
| From: ghc-devs-bounces <at> haskell.org [mailto:ghc-devs-bounces <at> haskell.org]
| On Behalf Of Joachim Breitner
| Sent: 11 July 2013 15:25
| To: ghc-devs <at> 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"
| and the plug the functions together by himself:
| https://github.com/nomeata/nt-coerce/blob/ec9b5/tests/LiftAbstract.hs

| 
| I also added a test suite to show what works already:
| https://github.com/nomeata/nt-coerce/tree/master/tests

| what does rightfully not work, due to abstraction:
| https://github.com/nomeata/nt-coerce/tree/master/tests/failing

| and what does not yet work, although it conceivably should:
| https://github.com/nomeata/nt-coerce/tree/master/tests/todo

| 
| The test suite contains expected output in *.out and *.err, so you can
| check out what happens without having to run it. The error messages are
| not yet as nice as they should be.
| 
| How to proceed from here Is this approach and design good enough to to
| into GHC, despite not being able to handle _all_ cases where it
| conceivably could, and the slight unwieldiness when coerctions for data
| types based on abstract data types?
| 
| BTW, I find it quite nice to be able to develop such a feature without
| touching GHC’s source. If that is possible for more contributions, the
| entry barrier to GHC would be noticeably lowered.
| 
| Thanks,
| Joachim
| 
| 
| --
| Joachim “nomeata” Breitner
|   mail <at> joachim-breitner.de • http://www.joachim-breitner.de/

|   Jabber: nomeata <at> joachim-breitner.de  • GPG-Key: 0x4743206C
|   Debian Developer: nomeata <at> debian.org
_______________________________________________
ghc-devs mailing list
ghc-devs <at> haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs
Simon Peyton-Jones | 15 Jul 23:57 2013
Picon

RE: Exposing newtype coercions to Haskell

Joachim

 

Discussing with Richard Eisenberg, we wondered the following.

 

·        note that the “seq” nonsense is because we allow user-defined NT-values

·        also note that to determine which NT values we can derive from in-scope NT values, we have to do something very similar to type-class solving.  Eg. need NT [T] [S], have available ntList :: forall ab. NT a b -> NT [a] [b], so use ntList to simplify NT [T] [S] to NT T S.

 

Hence the following suggestion: revert from NT as a data value to NT as a class.  Thus

          class NT a b where

            castNT :: a -> b

            uncastNT :: b -> a

 

Now when you have a data type you can say “deriving( NT )”, or things like

          deriving NT a b => NT [a] [b]

and expect the usual type-class deriving mechanism to do the job.

 

As usual, you can only do this if you can see the data constructor of the relevant type.

 

Now, you can say things like

          newtype Age = MkAge Int

          f :: [Age] -> Int

          f xs = sum (uncastNT xs)

and it’ll work fine.  If you omitted the type annotation on f you’d get something like

          f :: (Num a, NT [a] b) => b -> a

which is probably OK.

 

You might worry that instances are not scopeable.  Quite right.  If you make an NT instance, *everyone* can see it. So don’t make a type an instance of NT unless that’s want.  This is not terrible; it just means that you can’t make *local* NT instances, just as you can’t make local Eq instances.

 

This seems to involve a lot less special pleading than before, while still allowing the control you need.  For example, for Map you might say

          deriving instance NT a b => NT (Map k a) (Map k b)

 

The *derived* NT instances would be implemented, just as now, with lifted coercions.

 

You cannot write your own NT instance, just as you can’t write your own Typable instance.  That means we don’t need to worry about those bogus instances.

 

Does that make sense?

 

Simon

 

 

-----Original Message-----

From: ghc-devs-bounces <at> haskell.org [mailto:ghc-devs-bounces <at> haskell.org] On

Behalf Of Joachim Breitner

Sent: 11 July 2013 09:41

To: ghc-devs <at> haskell.org

Subject: Re: Exposing newtype coercions to Haskell

|  Hi,

|  Am Montag, den 08.07.2013, 09:39 +0000 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 are in scope, to preserve abstraction.

|  > | > It's not for soundness.

|  > |

|  > | I understand the approach, but I think it is insufficient. Assume

|  > | that the user wants to cheat for some reason and has this definition

|  > | for ntS, clearly writable without having access to S’s internals:

|  > |

|  > | ntS :: NT p p' -> NT q q' -> NT (S p q) (S p' q') ntS _ _ = error

|  > | "nah nah"

|  >

|  > Quite right!  My mistake was to say "if you CAN do that..." and then

|  > discard the evidence that you can do it.  What I should have said is

|  >

|  >    * prove a large bunch of NT constraints (one per constructor

|  >           field)

|  >    * then `seq` them

|  >    * before returning the "ordinary coercion lifting" result.

|  >

|  > The thing is, that the "ordinary coercion lifting" is sound (roles

|  > permitting -- should check that right off the bat).  But we are making

|  > a stronger check here, namely that the programmer has exported enough

|  > evidence, to expose abstractions.

|  Although it feels a bit weird to force one set of coercion witnesses (based on

|  datacon field types) and then use another (based on typecon parameters), it could

|  have worked, so I did more work in that direction, but I have hit another obstacle:

|  Just to clarify that we talk about the same things, an easy case:

|          data Family a = Family a a (List a)

|          deriving familyNT :: NT a b -> NT (Family a) (Family b) with "listNT :: NT a

|  b -> NT (List a) (List b)" in scope would get this

|  implementation:

|          familyNT nt = nt `seq` nt `seq` listNT nt `seq`

|                        case nt of (NT co -> NT (Family co)) This does ensure that, without

|  breaking abstractions, the user is allowed to convert the arguments of the datacon

|  and produces a sound coercion in in the F_C sense.

|  But what about a simple tree type?

|          data Tree a = Tree a (List (Tree a))

|          deriving treeNT :: NT a b -> NT (Tree a) (Tree b) I need to force witnesses

|  for

|        * (NT a b) (easy, that is the first argument) and for

|        * (NT (List (Tree a)) (NT (List (Tree b)).

|          The only way to obtain such a witness is to use listNT, which

|          would strictly(!) expect a value of type NT (Tree a) (Tree b),

|          which is what I am trying to produce at the moment, so I cannot

|          simply call treeNT.

|  In this case I can work around it by first creating the final NT value and then use it

|  to create and seq the witnesses required, before returning the result:

|          treeNT nt = let resNT = case nt of (NT co -> NT (Tree co))

|                      in nt `seq` listNT resNT `seq` resNT but this is becoming more and

|  more hacky and inelegant. For example, with mutually recursive data types, I’d

|  have to detect that they are mutually recursive and create similar witnesses in

|  advance for all involved types; for nested recursion I’d have to create multiple

|  witnesses, and who knows what else can happen.

|  From a logical point of view, I’d expect the coercion lifting for a recursive data type

|  to have a type like

|          a ~/C b -> (forall ta tb. (ta ~/C tb -> List ta ~/C List tb)) -> Tree a ~/C

|  Tree b (justified by writing the data type as a fixed point and thinking about fixed-

|  point induction), but its soundness breaks down immediately as the function type

|  -> in the second argument is not total.

|  That’s it for now,

|  Joachim

|  --

|  Joachim “nomeata” Breitner

|    mail <at> joachim-breitner.de • http://www.joachim-breitner.de/

|    Jabber: nomeata <at> joachim-breitner.de  • GPG-Key: 0x4743206C

|    Debian Developer: nomeata <at> debian.org

_______________________________________________
ghc-devs mailing list
ghc-devs@...
http://www.haskell.org/mailman/listinfo/ghc-devs
Joachim Breitner | 16 Jul 09:39 2013
Picon

Re: Exposing newtype coercions to Haskell

Hi,

Am Montag, den 15.07.2013, 21:57 +0000 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 we can derive from
> in-scope NT values, we have to do something very similar to type-class
> solving.  Eg. need NT [T] [S], have available ntList :: forall ab. NT
> a b -> NT [a] [b], so use ntList to simplify NT [T] [S] to NT T S.

Yes, as discussed.

> Hence the following suggestion: revert from NT as a data value to NT
> as a class.  Thus
> 
>           class NT a b where
>             castNT :: a -> b
>             uncastNT :: b -> a

We’ve discussed this proposal before. The only problem with it is that
it will not allow the author of a type container which should be
abstract to cast it in internal code; if that is ok then type classes
are definitely the nicer way.

I assume that the “real” NT class will be abstract and castNT/uncastNT
exposed as normal functions, not class methods, so that the user does
not create custom instances, right?

> You might worry that instances are not scopeable.  Quite right.  If
> you make an NT instance, *everyone* can see it. So don’t make a type
> an instance of NT unless that’s want.  This is not terrible; it just
> means that you can’t make *local* NT instances, just as you can’t make
> local Eq instances.

The thing is that I don’t need local Eq instances; I can just call my
local private myCustomEq. But I cannot create a local private coercion. 

I guess one can argue that if someone has such special needs, he will be
able to figure out when to use unsafeCoerce, and just let them play in
the rough outsides. So the missing feature can at least functionally
approximated (just as it can be now).

> Does that make sense?

Nothing new here besides the point that the feature „private, unexposed
NT coercions“ do not warrant the extra overhead of introducing new
syntax and replicating the deriving feature on the function level, and
I’ll take that point.

I guess it doesn’t change the implementation a lot, although I probably
can’t implement that in a plugin any more. Although it would actually be
a useful thing if code for deriving new type classes can be added in a
plugin :-)

So I’ll soon start implementing that.

Greetings,
Joachim

--

-- 
Joachim “nomeata” Breitner
  mail@...http://www.joachim-breitner.de/
  Jabber: nomeata@...  • GPG-Key: 0x4743206C
  Debian Developer: nomeata@...
_______________________________________________
ghc-devs mailing list
ghc-devs@...
http://www.haskell.org/mailman/listinfo/ghc-devs
Simon Peyton-Jones | 16 Jul 09:54 2013
Picon

RE: Exposing newtype coercions to Haskell

| 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 proposal before. The only problem with it is that
| it will not allow the author of a type container which should be
| abstract to cast it in internal code; if that is ok then type classes
| are definitely the nicer way.

OK. 

The whole story is *so* much simpler if we piggy back on type classes that I think that's a much better way to
go.  OK, so you can't do "deep casting" of internal data types without exposing the ability to "deep cast" to
clients.  But we have no convincing examples of such a need.

Let's do the simple thing.

| 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 new type-class-like deduction algorithm.  It all just
plays out through the existing type class machinery.

| Although it would actually be
| a useful thing if code for deriving new type classes can be added in a
| plugin :-)

Indeed. One answer is "generics".  Another is to have a mechanism for a front-end plugin.  But let's not bend
this feature out of shape to serve that goal. Better to design a better plugin mechanism.

Simon
_______________________________________________
ghc-devs mailing list
ghc-devs <at> haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs
Joachim Breitner | 16 Jul 10:02 2013
Picon

Re: Exposing newtype coercions to Haskell

Hi,

Am Dienstag, den 16.07.2013, 07:54 +0000 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 new type-class-like deduction algorithm.  It
> all just plays out through the existing type class machinery.

Ok, I was referring here to what I have done so far, which is mostly the
code that traverses the type and assembles the ~/C witness, which will
still be required.

Greetings,
Joachim

--

-- 
Joachim Breitner
  e-Mail: mail@...
  Homepage: http://www.joachim-breitner.de
  ICQ#: 74513189
  Jabber-ID: nomeata@...
_______________________________________________
ghc-devs mailing list
ghc-devs@...
http://www.haskell.org/mailman/listinfo/ghc-devs
Joachim Breitner | 22 Jul 14:06 2013
Picon

Re: Exposing newtype coercions to Haskell

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 :: a ~# Concrete a

but that does not work, as methods seem to need to have a boxed type.
Using "a ~ Concrete a" does not work as well, as that has kind
Constraint. So I wrapped ~# myself and created:

        data NT a b = NT ((~#) a b)
        class IsNT a where
            type Concrete a
            coercion :: NT a (Concrete a)

with only IsNT (I’ll think more about the name ;-)) and probably
Concrete exposed; not or coercion. The interface would then be functions

        castNT :: IsNT a => Concrete a -> a
        uncastNT :: IsNT a => a -> Concrete a

Now we want the user to be able to specify

        deriving instance IsNT Age -- with Concrete Age = Int
        deriving instance IsNT a => IsNT [a] -- with Concrete [a] = [Concrete a]
        deriving instance IsNT v => IsNT (Map k v) -- dito
and probably also
        deriving instance IsNT Int -- with Concrete Int = Int
for all non-newtypes.

After adding the definitions to ghc-prim and extending PrelNames I tried
to make the deriving code, starting with the last examle (IsNT Int).
There, the generated code should be something like 

        instance IsNT Int where
        	type Concrete Int = Int
        	coercion = NT (refl Int)

But here I am stuck: The deriving code mechanism expects me to give the
method definitions as HsExpr, but I’d like to generate Core here. How
can I achieve that, or what other options do I have?

(Of course this will need further adjustments when Richard’s role code
is in.)

(If there is a reason to go back to the two parameter type class "NT a
b", no problem, but the problem of HsExpr vs. CoreExpr would still
remain.)

Greetings,
Joachim

--

-- 
Joachim “nomeata” Breitner
  mail@...http://www.joachim-breitner.de/
  Jabber: nomeata@...  • GPG-Key: 0x4743206C
  Debian Developer: nomeata@...
_______________________________________________
ghc-devs mailing list
ghc-devs@...
http://www.haskell.org/mailman/listinfo/ghc-devs
Richard Eisenberg | 22 Jul 18:01 2013

Re: Exposing newtype coercions to Haskell

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 instance IsNT ...".

- The type that you've called NT below will soon exist in base, in the 
module Data.Type.Equality. See 
http://ghc.haskell.org/trac/ghc/wiki/TypeLevelReasoning  That 
implementation ran into a little bump this morning, but it should be 
pushed within 24 hours.

- 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: 
http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf  I hope 
to have an implementation of the ideas in that paper available later 
this week. There are some user-facing features, about which there will 
be wiki page some point quite soon.) A nominal coercion should only 
exist between two types that are nominally equal. Under this definition 
Age and Int are not nominally equal, because they have different names. 
The other interesting equality is "representational". This equality 
considers Age and Int to be representationally equal, because they have 
the same representation. A key point of newtype coercions is that they 
work over representational equality, not only nominal equality. Working 
over representational equality is what makes them interesting and 
useful. Currently, there is no way to abstract over representational 
coercions -- that is, there
is no way to store one, say in a GADT or other Haskelly data type. Of 
course, a data structure within GHC can store a representational 
coercion; you just can't have one be the payload of an Id, say. So, that 
means that the implementation of newtype coercions may have to be a 
little more magical than the design you're writing. Or, it's possible 
that we could add abstraction over representational coercions, but I 
prefer the magical approach, because I don't see a general need for the 
ability to abstract.

Now that I think of it, you may need to generalize the deriving 
mechanism a bit. All current "deriving"s generate code that the user 
could write. (Typeable is something of an exception here.) Here, the 
generated code is something that a user can not write. Maybe that's why 
you wanted CoreExprs in the first place!

Somewhat separately:

- I prefer the two-parameter class over a one-parameter, as it seems 
more flexible. If the two-parameter version (without any dependencies 
between the two parameters) hinders type inference, users can define an 
explicitly-typed wrapper. Why do I want this flexibility? Because, once 
roles are done, the following should be possible:

> data Foo a = MkFoo
> deriving instance IsNT (Foo a) (Foo b)

Note that `a` is a phantom parameter here, and, yes, I meant `data` 
there, not newtype. In other news, I would prefer the name not to 
mention newtypes, because I think the mechanism is somewhat stronger 
than just newtype coercions.

Richard

On 2013-07-22 13:06, Joachim Breitner wrote:
> 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 :: a ~# Concrete a
> 
> but that does not work, as methods seem to need to have a boxed type.
> Using "a ~ Concrete a" does not work as well, as that has kind
> Constraint. So I wrapped ~# myself and created:
> 
>         data NT a b = NT ((~#) a b)
>         class IsNT a where
>             type Concrete a
>             coercion :: NT a (Concrete a)
> 
> with only IsNT (I’ll think more about the name ;-)) and probably
> Concrete exposed; not or coercion. The interface would then be 
> functions
> 
>         castNT :: IsNT a => Concrete a -> a
>         uncastNT :: IsNT a => a -> Concrete a
> 
> Now we want the user to be able to specify
> 
>         deriving instance IsNT Age -- with Concrete Age = Int
>         deriving instance IsNT a => IsNT [a] -- with Concrete [a] = 
> [Concrete a]
>         deriving instance IsNT v => IsNT (Map k v) -- dito
> and probably also
>         deriving instance IsNT Int -- with Concrete Int = Int
> for all non-newtypes.
> 
> After adding the definitions to ghc-prim and extending PrelNames I 
> tried
> to make the deriving code, starting with the last examle (IsNT Int).
> There, the generated code should be something like
> 
>         instance IsNT Int where
>         	type Concrete Int = Int
>         	coercion = NT (refl Int)
> 
> But here I am stuck: The deriving code mechanism expects me to give the
> method definitions as HsExpr, but I’d like to generate Core here. How
> can I achieve that, or what other options do I have?
> 
> (Of course this will need further adjustments when Richard’s role code
> is in.)
> 
> (If there is a reason to go back to the two parameter type class "NT a
> b", no problem, but the problem of HsExpr vs. CoreExpr would still
> remain.)
> 
> Greetings,
> Joachim
> 
> _______________________________________________
> ghc-devs mailing list
> ghc-devs <at> haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
ghc-devs <at> haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs
Simon Peyton-Jones | 23 Jul 07:23 2013
Picon

RE: Exposing newtype coercions to Haskell

|  - 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
	deriving instance (NT a b) => NT [a] [b]

The whole point of what Joachim is studying is making it possible for the programmer to generate
representational equalities, and use them with ntCast.  
	ntCast :: NT a b -> a -> b
(I'm ignoring the question about the final names for things.)  So we can't use the new (:=:) type because it
wraps nominal equality.  To work with the approach Joachim sketches we'd need:

	data REq a b where
 	   REq :: (a ~R# b) -> NT a b

which wraps a *representational* equality.  But as you say, we weren't planning to abstract over
representational equalities at all in FC, so that would bring up a range of questions.   One possible
response is that we *should* allow abstraction over ~R; there's nothing wrong with it in principle, it's
just that we didn't think it was necessary.  The main cost is that we'd need an unboxed type constructor ~R#
(to match the existing ~# which is really nominal equalty ~N#), and a boxed one (called NT above) to match (:=:).

So the above instance declaration would somehow generate

	ntList :: REq a b -> REq [a] [b]
	ntList (REq (c :: a  ~R#  b)) = REq ([c] :: [a]  ~R#  [b])

You mention a "magical" approach, but I'm not sure what that is.

The question of how to represent all this in HsSyn, to communicate between TcDeriv and TcInstDcls, is a
somewhat separate matter.  We can solve that in several ways.  But first we need be sure what the FC story is.

My instinct is for a 2-param type class.  For 'newtype Age = MkAge Int', it seems odd to have both the newtype axiom
	axiom ax4 : Age ~ Int
and a type family axiom
	axiom ax5 Concrete Age ~ Int

Simon

 A nominal coercion should only
|  exist between two types that are nominally equal. Under this definition
|  Age and Int are not nominally equal, because they have different names.
|  The other interesting equality is "representational". This equality
|  considers Age and Int to be representationally equal, because they have
|  the same representation. A key point of newtype coercions is that they
|  work over representational equality, not only nominal equality. Working
|  over representational equality is what makes them interesting and
|  useful. Currently, there is no way to abstract over representational
|  coercions -- that is, there
|  is no way to store one, say in a GADT or other Haskelly data type. Of
|  course, a data structure within GHC can store a representational
|  coercion; you just can't have one be the payload of an Id, say. So, that
|  means that the implementation of newtype coercions may have to be a
|  little more magical than the design you're writing. Or, it's possible
|  that we could add abstraction over representational coercions, but I
|  prefer the magical approach, because I don't see a general need for the
|  ability to abstract.
|  
|  Now that I think of it, you may need to generalize the deriving
|  mechanism a bit. All current "deriving"s generate code that the user
|  could write. (Typeable is something of an exception here.) Here, the
|  generated code is something that a user can not write. Maybe that's why
|  you wanted CoreExprs in the first place!
|  
|  Somewhat separately:
|  
|  - I prefer the two-parameter class over a one-parameter, as it seems
|  more flexible. If the two-parameter version (without any dependencies
|  between the two parameters) hinders type inference, users can define an
|  explicitly-typed wrapper. Why do I want this flexibility? Because, once
|  roles are done, the following should be possible:
|  
|  > data Foo a = MkFoo
|  > deriving instance IsNT (Foo a) (Foo b)
|  
|  Note that `a` is a phantom parameter here, and, yes, I meant `data`
|  there, not newtype. In other news, I would prefer the name not to
|  mention newtypes, because I think the mechanism is somewhat stronger
|  than just newtype coercions.
|  
|  Richard
|  
|  On 2013-07-22 13:06, Joachim Breitner wrote:
|  > 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 :: a ~# Concrete a
|  >
|  > but that does not work, as methods seem to need to have a boxed type.
|  > Using "a ~ Concrete a" does not work as well, as that has kind
|  > Constraint. So I wrapped ~# myself and created:
|  >
|  >         data NT a b = NT ((~#) a b)
|  >         class IsNT a where
|  >             type Concrete a
|  >             coercion :: NT a (Concrete a)
|  >
|  > with only IsNT (I’ll think more about the name ;-)) and probably
|  > Concrete exposed; not or coercion. The interface would then be
|  > functions
|  >
|  >         castNT :: IsNT a => Concrete a -> a
|  >         uncastNT :: IsNT a => a -> Concrete a
|  >
|  > Now we want the user to be able to specify
|  >
|  >         deriving instance IsNT Age -- with Concrete Age = Int
|  >         deriving instance IsNT a => IsNT [a] -- with Concrete [a] =
|  > [Concrete a]
|  >         deriving instance IsNT v => IsNT (Map k v) -- dito
|  > and probably also
|  >         deriving instance IsNT Int -- with Concrete Int = Int
|  > for all non-newtypes.
|  >
|  > After adding the definitions to ghc-prim and extending PrelNames I
|  > tried
|  > to make the deriving code, starting with the last examle (IsNT Int).
|  > There, the generated code should be something like
|  >
|  >         instance IsNT Int where
|  >         	type Concrete Int = Int
|  >         	coercion = NT (refl Int)
|  >
|  > But here I am stuck: The deriving code mechanism expects me to give the
|  > method definitions as HsExpr, but I’d like to generate Core here. How
|  > can I achieve that, or what other options do I have?
|  >
|  > (Of course this will need further adjustments when Richard’s role code
|  > is in.)
|  >
|  > (If there is a reason to go back to the two parameter type class "NT a
|  > b", no problem, but the problem of HsExpr vs. CoreExpr would still
|  > remain.)
|  >
|  > Greetings,
|  > Joachim
|  >
|  > _______________________________________________
|  > ghc-devs mailing list
|  > ghc-devs <at> haskell.org
|  > http://www.haskell.org/mailman/listinfo/ghc-devs

|  
|  _______________________________________________
|  ghc-devs mailing list
|  ghc-devs <at> haskell.org
|  http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
ghc-devs <at> haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs
Joachim Breitner | 23 Jul 09:21 2013
Picon

Re: Exposing newtype coercions to Haskell

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 allows nice error messages to be reported at 
> the site of a user's "deriving instance IsNT ...".

My plan was to make all checks (constructors in scope; IsNT classes for
all data constructor arguments present) in TcDeriv, so you get nice
error messages. If it turns out that the actual coercion can only be
generated in a later pass, then it the checks just need to be strong
enough to make that pass always succeed.

> - 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.

I know; I was just using them until representational equality is in and
plan to switch then. 

>  (Nominal coercions correspond to the "C" coercions from this paper)

I got confused by C and T in my previous mails. In any case, I am only
concerned with representational equality (T, it seems) for this project.

> Or, it's possible 
> that we could add abstraction over representational coercions, but I 
> prefer the magical approach, because I don't see a general need for the 
> ability to abstract.

Hmm, I must admit I was assuming that once the roles implementation is
in there will be ~# and ~#/T (or ~R#, which is a less-easy-to-confuse
moniker) available in Core.

> Now that I think of it, you may need to generalize the deriving 
> mechanism a bit. All current "deriving"s generate code that the user 
> could write. (Typeable is something of an exception here.) Here, the 
> generated code is something that a user can not write. Maybe that's why 
> you wanted CoreExprs in the first place!

Exactly. But it is also the reason why we are aiming for deriving
classes (and not NT values), because it is already an established way of
having the compiler generate code for you.

> - I prefer the two-parameter class over a one-parameter, as it seems 
> more flexible. 

Thanks for spotting the phantom type replacing example, which is a
features I’d also like to have. The type family was just a quick idea
(and it would be neat to be able to ask GHCi via ":kind! (Concrete t)"
what t looks like with all newtypes unfolded), but it’s not worth the
loss of flexibility.

In some cases, the type family might require less type annotations.
Consider
newtype Age = Age Int
newtype NT1 = NT1 Int
newtype NT2 = NT2 Int

myCast :: Either NT1 Age -> Either NT2 Age
myCast = castNT . uncastNT

With two parameters, GHC will not know whether it should cast via
"Either Int Age" or "Either Int Int", while with a type family there
will be only one choice, "Concrete (Either NT1 Age) = Either Int Int".
In general, castNT . uncastNT would have the nice type
        castNT . uncastNT  :: Concrete a ~ Concrete b => a -> b
which plainly expresses „Cast between any to values who have the same
concrete representation.“. Just as a side remark in case this comes up
later again.

BTW, what should the base-case be? I believe most user-friendly is a
least-specific class
        instance IsNT a a
so that the cast "Either Age a -> Either Int a" is possible. Or are
overlapping instances too bad and the user should derive instances for
all non-container non-newtype types himself:
        instance IsNT Int Int ....

Am Dienstag, den 23.07.2013, 05:23 +0000 schrieb Simon Peyton-Jones:
> The question of how to represent all this in HsSyn, to communicate
> between TcDeriv and TcInstDcls, is a somewhat separate matter.  We can
> solve that in several ways.  But first we need be sure what the FC
> story is.

For now what I am doing is that in TcDeriv, I am implementing the method
with a value "unfinishedNTInstance :: a" which I am then replacing in a
always-run simplCore pass with the real implementation in Core. It is a
work-around that lets me explore the design-space and implementation
issues without having to rewire GHC.

Greetings,
Joachim

--

-- 
Joachim “nomeata” Breitner
  mail@...http://www.joachim-breitner.de/
  Jabber: nomeata@...  • GPG-Key: 0x4743206C
  Debian Developer: nomeata@...
_______________________________________________
ghc-devs mailing list
ghc-devs@...
http://www.haskell.org/mailman/listinfo/ghc-devs
Richard Eisenberg | 23 Jul 10:51 2013

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 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 this 
in Core?

> class NT a b = MkNT { castNT :: a -> b ; uncastNT :: b -> a }
> NTCo:Age :: Age ~R# Int         -- see [1]
> NTAgeInst :: NT Age Int
> NTAgeInst = MkNT { castNT = \(a :: Age). a |> NTCo:Age ; uncastNT = \(x 
> :: Int). x |> sym NTCo:Age }

[1]: We still do have representational coercions, even though it would 
be bogus to extract their type, as the type constructor ~R# does not 
exist. But, coercionKind, which returns the two coerced types, and the 
new coercionRole (which would return Representational in this case) work 
just fine.

Here, we don't need to abstract over ~R#, by just referring to the 
global axiom directly. Does this compose well? I think so; you'll just 
have to inline all of the coercions. But, the coercions won't ever get 
too big, as they will always mirror exactly the structure of the types 
being coerced. Simon, this is the sort of "magic" I was thinking of, 
magical because I can't imagine a way this could be produced from an 
HsExpr.

Also, nice example of how the one-parameter design might aid the 
programmer. 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.

Richard

On 2013-07-23 08:21, Joachim Breitner wrote:
> 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 allows nice error messages to be reported at
>> the site of a user's "deriving instance IsNT ...".
> 
> My plan was to make all checks (constructors in scope; IsNT classes for
> all data constructor arguments present) in TcDeriv, so you get nice
> error messages. If it turns out that the actual coercion can only be
> generated in a later pass, then it the checks just need to be strong
> enough to make that pass always succeed.
> 
>> - 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.
> 
> I know; I was just using them until representational equality is in and
> plan to switch then.
> 
>>  (Nominal coercions correspond to the "C" coercions from this paper)
> 
> I got confused by C and T in my previous mails. In any case, I am only
> concerned with representational equality (T, it seems) for this 
> project.
> 
>> Or, it's possible
>> that we could add abstraction over representational coercions, but I
>> prefer the magical approach, because I don't see a general need for 
>> the
>> ability to abstract.
> 
> Hmm, I must admit I was assuming that once the roles implementation is
> in there will be ~# and ~#/T (or ~R#, which is a less-easy-to-confuse
> moniker) available in Core.
> 
> 
>> Now that I think of it, you may need to generalize the deriving
>> mechanism a bit. All current "deriving"s generate code that the user
>> could write. (Typeable is something of an exception here.) Here, the
>> generated code is something that a user can not write. Maybe that's 
>> why
>> you wanted CoreExprs in the first place!
> 
> Exactly. But it is also the reason why we are aiming for deriving
> classes (and not NT values), because it is already an established way 
> of
> having the compiler generate code for you.
> 
> 
>> - I prefer the two-parameter class over a one-parameter, as it seems
>> more flexible.
> 
> Thanks for spotting the phantom type replacing example, which is a
> features I’d also like to have. The type family was just a quick idea
> (and it would be neat to be able to ask GHCi via ":kind! (Concrete t)"
> what t looks like with all newtypes unfolded), but it’s not worth the
> loss of flexibility.
> 
> 
> In some cases, the type family might require less type annotations.
> Consider
> newtype Age = Age Int
> newtype NT1 = NT1 Int
> newtype NT2 = NT2 Int
> 
> myCast :: Either NT1 Age -> Either NT2 Age
> myCast = castNT . uncastNT
> 
> With two parameters, GHC will not know whether it should cast via
> "Either Int Age" or "Either Int Int", while with a type family there
> will be only one choice, "Concrete (Either NT1 Age) = Either Int Int".
> In general, castNT . uncastNT would have the nice type
>         castNT . uncastNT  :: Concrete a ~ Concrete b => a -> b
> which plainly expresses „Cast between any to values who have the same
> concrete representation.“. Just as a side remark in case this comes up
> later again.
> 
> 
> 
> BTW, what should the base-case be? I believe most user-friendly is a
> least-specific class
>         instance IsNT a a
> so that the cast "Either Age a -> Either Int a" is possible. Or are
> overlapping instances too bad and the user should derive instances for
> all non-container non-newtype types himself:
>         instance IsNT Int Int ....
> 
> 
> Am Dienstag, den 23.07.2013, 05:23 +0000 schrieb Simon Peyton-Jones:
>> The question of how to represent all this in HsSyn, to communicate
>> between TcDeriv and TcInstDcls, is a somewhat separate matter.  We can
>> solve that in several ways.  But first we need be sure what the FC
>> story is.
> 
> For now what I am doing is that in TcDeriv, I am implementing the 
> method
> with a value "unfinishedNTInstance :: a" which I am then replacing in a
> always-run simplCore pass with the real implementation in Core. It is a
> work-around that lets me explore the design-space and implementation
> issues without having to rewire GHC.
> 
> Greetings,
> Joachim
> 
> 
> _______________________________________________
> ghc-devs mailing list
> ghc-devs <at> haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
ghc-devs <at> haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs
Joachim Breitner | 23 Jul 11:00 2013
Picon

Re: Exposing newtype coercions to Haskell

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'm still not 
> convinced we need it for newtype coercions, though. What if we have this 
> in Core?
> 
> > class NT a b = MkNT { castNT :: a -> b ; uncastNT :: b -> a }
> > NTCo:Age :: Age ~R# Int         -- see [1]
> > NTAgeInst :: NT Age Int
> > NTAgeInst = MkNT { castNT = \(a :: Age). a |> NTCo:Age ; uncastNT = \(x 
> > :: Int). x |> sym NTCo:Age }

I thought about this class definition, and it is has the nice property
that we can actually implement the methods by hand (without the
zero-cost of course), which would be a good lint-like check that we do
not generate illegal instances. The problem is that It it would not
allow
deriving instance NT a b => NT [a] [b]
as there is no way to extract the coercion that was used in the
implementation of NT a b. Hence the need to expose (to Core, not to tue
user) the coercion in the class: The cast operations do not compose
well.

Greetings,
Joachim

--

-- 
Joachim “nomeata” Breitner
  mail@...http://www.joachim-breitner.de/
  Jabber: nomeata@...  • GPG-Key: 0x4743206C
  Debian Developer: nomeata@...
_______________________________________________
ghc-devs mailing list
ghc-devs@...
http://www.haskell.org/mailman/listinfo/ghc-devs
Richard Eisenberg | 23 Jul 12:43 2013

Re: Exposing newtype coercions to Haskell

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:
>> 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 
>> this
>> in Core?
>> 
>> > class NT a b = MkNT { castNT :: a -> b ; uncastNT :: b -> a }
>> > NTCo:Age :: Age ~R# Int         -- see [1]
>> > NTAgeInst :: NT Age Int
>> > NTAgeInst = MkNT { castNT = \(a :: Age). a |> NTCo:Age ; uncastNT = \(x
>> > :: Int). x |> sym NTCo:Age }
> 
> I thought about this class definition, and it is has the nice property
> that we can actually implement the methods by hand (without the
> zero-cost of course), which would be a good lint-like check that we do
> not generate illegal instances. The problem is that It it would not
> allow
> deriving instance NT a b => NT [a] [b]
> as there is no way to extract the coercion that was used in the
> implementation of NT a b. Hence the need to expose (to Core, not to tue
> user) the coercion in the class: The cast operations do not compose
> well.
> 
> Greetings,
> Joachim
> 
> _______________________________________________
> ghc-devs mailing list
> ghc-devs@...
> http://www.haskell.org/mailman/listinfo/ghc-devs
Joachim Breitner | 23 Jul 13:45 2013
Picon

Re: Exposing newtype coercions to Haskell

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-class-approach.

tl;dr: "IsNT a a" only works with IncoherentInstances, which are in 
       principle fine for this class (it is univalent in a sense), but 
       requiring this extension would be quite unfortunate.

Consider this ghci session (this already works here):

Prelude GHC.NT> newtype Age = Age Int deriving Show
Prelude GHC.NT> deriving instance IsNT Int Age
Prelude GHC.NT> castNT (1::Int) :: Age -- good, works
Age 1
Prelude GHC.NT> deriving instance (IsNT a a', IsNT b b') => IsNT (Either a b) (Either a' b')
Prelude GHC.NT> castNT (Left 1::Either Int Int) :: Either Age Age -- also works
Left (Age 1)
Prelude GHC.NT> castNT (Left 1::Either Int Int) :: Either Age Int -- does not work yet

<interactive>:12:1:
    No instance for (IsNT Int Int) arising from a use of ‛castNT’
    In the expression:
        castNT (Left 1 :: Either Int Int) :: Either Age Int
    In an equation for ‛it’:
        it = castNT (Left 1 :: Either Int Int) :: Either Age Int
Prelude GHC.NT> deriving instance IsNT Int Int
Prelude GHC.NT> castNT (Left 1::Either Int Int) :: Either Age Int -- works now
Left (Age 1)
Prelude GHC.NT> :t castNT :: (Either Int Int) -> (Either Age Int)
castNT :: (Either Int Int) -> (Either Age Int) :: Either Int Int -> Either Age Int

But we are not able to cast such that one type parameter changes while
leaving another type _variable_ untouched:

Prelude GHC.NT> :t  castNT :: (Either Int a) -> (Either Age a)

<interactive>:1:1:
    No instance for (IsNT a1 a1) arising from a use of ‛castNT’
    Possible fix:
      add (IsNT a1 a1) to the context of
        an expression type signature: Either Int a1 -> Either Age a1
        or the inferred type of it :: Either Int a -> Either Age a
    In the expression: castNT :: (Either Int a) -> (Either Age a)

and if we add "IsNT a a" as a base case:

Prelude GHC.NT> instance IsNT a a

<interactive>:34:10: Warning:
    No explicit method or default declaration for ‛coercion’
    In the instance declaration for ‛IsNT a a’

we get

Prelude GHC.NT> :t  castNT :: (Either Int a) -> (Either Age a)

<interactive>:1:1:
    Overlapping instances for IsNT a1 a1 arising from a use of ‛castNT’
    Matching instances:
      instance [overlap ok] IsNT a a -- Defined at <interactive>:34:10
      instance IsNT Int Int -- Defined at <interactive>:13:1
      instance (IsNT a a', IsNT b b') => IsNT (Either a b) (Either a' b')
        -- Defined at <interactive>:10:1
    (The choice depends on the instantiation of ‛a1’
     To pick the first instance above, use -XIncoherentInstances
     when compiling the other instance declarations)
    In the expression: castNT :: (Either Int a) -> (Either Age a)

Re-doing the session with -XIncoherentInstances set helps, but requiring
that for every module that wants to derive a IsNT class is probably not
nice.

The one-parameter-variant does not help either.

One way to avoid the issue is to have two instances for Either:

Prelude GHC.NT> deriving instance (IsNT a a') => IsNT (Either a b) (Either a' b)
Prelude GHC.NT> deriving instance (IsNT b b') => IsNT (Either a b) (Either a b')

This still requires OverlappingInstances, but I can get the desired cast
without IncoherentInstances:

Prelude GHC.NT> :t castNT :: Either Int a -> Either Age a
castNT :: Either Int a -> Either Age a
  :: Either Int a -> Either Age a

Other casts that should be “normal” are more complicated now:

Prelude GHC.NT> let c = (castNT :: Either Age Int -> Either Age Age) . (castNT :: Either Int Int -> Either Age Int)
Prelude GHC.NT> :t c
c :: Either Int Int -> Either Age Age
Prelude GHC.NT> c (Left 1)
Left (Age 1)

In any case, the whole thing needs a bit more massaging until it becomes
sufficiently elegant.

Greetings,
Joachim

--

-- 
Joachim Breitner
  e-Mail: mail@...
  Homepage: http://www.joachim-breitner.de
  ICQ#: 74513189
  Jabber-ID: nomeata@...
_______________________________________________
ghc-devs mailing list
ghc-devs@...
http://www.haskell.org/mailman/listinfo/ghc-devs
Simon Peyton-Jones | 23 Jul 20:58 2013
Picon

RE: Exposing newtype coercions to Haskell

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 instance".  You don't need the flag in importing modules.

I think that's fine.  For the IsNT class, where users cannot define their own instances, it really is not
incoherent to pick the IsNT a a instance.  The operational effect is always a no-op.

In short, I think this'll work fine.

Simon

|  -----Original Message-----
|  From: ghc-devs [mailto:ghc-devs-bounces <at> haskell.org] On Behalf Of Joachim
|  Breitner
|  Sent: 23 July 2013 12:45
|  To: ghc-devs <at> 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 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-class-approach.
|  
|  tl;dr: "IsNT a a" only works with IncoherentInstances, which are in
|         principle fine for this class (it is univalent in a sense), but
|         requiring this extension would be quite unfortunate.
|  
|  
|  Consider this ghci session (this already works here):
|  
|  Prelude GHC.NT> newtype Age = Age Int deriving Show
|  Prelude GHC.NT> deriving instance IsNT Int Age
|  Prelude GHC.NT> castNT (1::Int) :: Age -- good, works
|  Age 1
|  Prelude GHC.NT> deriving instance (IsNT a a', IsNT b b') => IsNT (Either a b)
|  (Either a' b')
|  Prelude GHC.NT> castNT (Left 1::Either Int Int) :: Either Age Age -- also works
|  Left (Age 1)
|  Prelude GHC.NT> castNT (Left 1::Either Int Int) :: Either Age Int -- does not work
|  yet
|  
|  <interactive>:12:1:
|      No instance for (IsNT Int Int) arising from a use of ‛castNT’
|      In the expression:
|          castNT (Left 1 :: Either Int Int) :: Either Age Int
|      In an equation for ‛it’:
|          it = castNT (Left 1 :: Either Int Int) :: Either Age Int
|  Prelude GHC.NT> deriving instance IsNT Int Int
|  Prelude GHC.NT> castNT (Left 1::Either Int Int) :: Either Age Int -- works now
|  Left (Age 1)
|  Prelude GHC.NT> :t castNT :: (Either Int Int) -> (Either Age Int)
|  castNT :: (Either Int Int) -> (Either Age Int) :: Either Int Int -> Either Age Int
|  
|  But we are not able to cast such that one type parameter changes while
|  leaving another type _variable_ untouched:
|  
|  Prelude GHC.NT> :t  castNT :: (Either Int a) -> (Either Age a)
|  
|  <interactive>:1:1:
|      No instance for (IsNT a1 a1) arising from a use of ‛castNT’
|      Possible fix:
|        add (IsNT a1 a1) to the context of
|          an expression type signature: Either Int a1 -> Either Age a1
|          or the inferred type of it :: Either Int a -> Either Age a
|      In the expression: castNT :: (Either Int a) -> (Either Age a)
|  
|  and if we add "IsNT a a" as a base case:
|  
|  Prelude GHC.NT> instance IsNT a a
|  
|  <interactive>:34:10: Warning:
|      No explicit method or default declaration for ‛coercion’
|      In the instance declaration for ‛IsNT a a’
|  
|  we get
|  
|  Prelude GHC.NT> :t  castNT :: (Either Int a) -> (Either Age a)
|  
|  <interactive>:1:1:
|      Overlapping instances for IsNT a1 a1 arising from a use of ‛castNT’
|      Matching instances:
|        instance [overlap ok] IsNT a a -- Defined at <interactive>:34:10
|        instance IsNT Int Int -- Defined at <interactive>:13:1
|        instance (IsNT a a', IsNT b b') => IsNT (Either a b) (Either a' b')
|          -- Defined at <interactive>:10:1
|      (The choice depends on the instantiation of ‛a1’
|       To pick the first instance above, use -XIncoherentInstances
|       when compiling the other instance declarations)
|      In the expression: castNT :: (Either Int a) -> (Either Age a)
|  
|  
|  Re-doing the session with -XIncoherentInstances set helps, but requiring
|  that for every module that wants to derive a IsNT class is probably not
|  nice.
|  
|  
|  The one-parameter-variant does not help either.
|  
|  
|  One way to avoid the issue is to have two instances for Either:
|  
|  Prelude GHC.NT> deriving instance (IsNT a a') => IsNT (Either a b) (Either a' b)
|  Prelude GHC.NT> deriving instance (IsNT b b') => IsNT (Either a b) (Either a b')
|  
|  This still requires OverlappingInstances, but I can get the desired cast
|  without IncoherentInstances:
|  
|  Prelude GHC.NT> :t castNT :: Either Int a -> Either Age a
|  castNT :: Either Int a -> Either Age a
|    :: Either Int a -> Either Age a
|  
|  Other casts that should be “normal” are more complicated now:
|  
|  Prelude GHC.NT> let c = (castNT :: Either Age Int -> Either Age Age) . (castNT ::
|  Either Int Int -> Either Age Int)
|  Prelude GHC.NT> :t c
|  c :: Either Int Int -> Either Age Age
|  Prelude GHC.NT> c (Left 1)
|  Left (Age 1)
|  
|  
|  
|  In any case, the whole thing needs a bit more massaging until it becomes
|  sufficiently elegant.
|  
|  Greetings,
|  Joachim
|  
|  --
|  Joachim Breitner
|    e-Mail: mail <at> joachim-breitner.de
|    Homepage: http://www.joachim-breitner.de

|    ICQ#: 74513189
|    Jabber-ID: nomeata <at> joachim-breitner.de
_______________________________________________
ghc-devs mailing list
ghc-devs <at> haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs
Joachim Breitner | 24 Jul 09:31 2013
Picon

Re: Exposing newtype coercions to Haskell

Hi,

Am Dienstag, den 23.07.2013, 18:58 +0000 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 instance".  You don't need the flag in importing
> modules.

That does not seem to be the case: Enabling the flag just for the
special "IsNT a a" instance does not work:

Prelude GHC.NT> :t  castNT :: (Either Int a) -> (Either Age a)

<interactive>:1:1:
    Overlapping instances for IsNT a1 a1 arising from a use of ‛castNT’
    Matching instances:
      instance [incoherent] IsNT a a -- Defined at <interactive>:12:10
      instance (IsNT a a', IsNT b b') => IsNT (Either a b) (Either a' b')
        -- Defined at <interactive>:7:1
    (The choice depends on the instantiation of ‛a1’
     To pick the first instance above, use -XIncoherentInstances
     when compiling the other instance declarations)
    In the expression: castNT :: (Either Int a) -> (Either Age a)

(as correctly specified by the error message.)

But now the solution is easy to see: When deriving IsNT, simply set the
incoherent flag for every instance, independent of any active pragmas.

Greetings,
Joachim

--

-- 
Joachim “nomeata” Breitner
  mail@...http://www.joachim-breitner.de/
  Jabber: nomeata@...  • GPG-Key: 0x4743206C
  Debian Developer: nomeata@...

_______________________________________________
ghc-devs mailing list
ghc-devs@...
http://www.haskell.org/mailman/listinfo/ghc-devs
Richard Eisenberg | 31 Jul 23:10 2013

Re: Exposing newtype coercions to Haskell

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. The Id stored in a
CoVarCo can usefully have a type headed by eqReprPrimTyCon.

If you're really eager to take a look, I use github to coordinate among computers; you can see the roles
branch at github.com/goldfirere/ghc.

Richard

On Jul 24, 2013, at 8:31 AM, Joachim Breitner wrote:

> Hi,
> 
> Am Dienstag, den 23.07.2013, 18:58 +0000 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 instance".  You don't need the flag in importing
>> modules.
> 
> That does not seem to be the case: Enabling the flag just for the
> special "IsNT a a" instance does not work:
> 
> 
> Prelude GHC.NT> :t  castNT :: (Either Int a) -> (Either Age a)
> 
> <interactive>:1:1:
>    Overlapping instances for IsNT a1 a1 arising from a use of ‛castNT’
>    Matching instances:
>      instance [incoherent] IsNT a a -- Defined at <interactive>:12:10
>      instance (IsNT a a', IsNT b b') => IsNT (Either a b) (Either a' b')
>        -- Defined at <interactive>:7:1
>    (The choice depends on the instantiation of ‛a1’
>     To pick the first instance above, use -XIncoherentInstances
>     when compiling the other instance declarations)
>    In the expression: castNT :: (Either Int a) -> (Either Age a)
> 
> (as correctly specified by the error message.)
> 
> 
> But now the solution is easy to see: When deriving IsNT, simply set the
> incoherent flag for every instance, independent of any active pragmas.
> 
> Greetings,
> Joachim
> 
> 
> 
> 
> -- 
> Joachim “nomeata” Breitner
>  mail <at> joachim-breitner.de • http://www.joachim-breitner.de/
>  Jabber: nomeata <at> joachim-breitner.de  • GPG-Key: 0x4743206C
>  Debian Developer: nomeata <at> debian.org
> 
> _______________________________________________
> ghc-devs mailing list
> ghc-devs <at> haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
ghc-devs <at> haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs
Simon Peyton-Jones | 23 Jul 20:46 2013
Picon

RE: Exposing newtype coercions to Haskell

I thought about the design you suggest below, but rejected it because I don't see how to do lifting -- which is
really the whole point! In particular, what are you going to write for

ntList :: NT a b -> NT [a] [b]
ntList (MkNT castNT uncastNT) = MkNT ??? ???

For lists you could write (fmap castNT), but the whole point of this exercise is not to write that -- and the
type might not be an instance of Functor.

I'm thinking we need (~R#) as a type constructor.

Simon

|  -----Original Message-----
|  From: ghc-devs [mailto:ghc-devs-bounces <at> haskell.org] On Behalf Of Richard
|  Eisenberg
|  Sent: 23 July 2013 09:51
|  To: Joachim Breitner
|  Cc: ghc-devs <at> 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 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 this
|  in Core?
|  
|  > class NT a b = MkNT { castNT :: a -> b ; uncastNT :: b -> a }
|  > NTCo:Age :: Age ~R# Int         -- see [1]
|  > NTAgeInst :: NT Age Int
|  > NTAgeInst = MkNT { castNT = \(a :: Age). a |> NTCo:Age ; uncastNT = \(x
|  > :: Int). x |> sym NTCo:Age }
|  
|  [1]: We still do have representational coercions, even though it would
|  be bogus to extract their type, as the type constructor ~R# does not
|  exist. But, coercionKind, which returns the two coerced types, and the
|  new coercionRole (which would return Representational in this case) work
|  just fine.
|  
|  Here, we don't need to abstract over ~R#, by just referring to the
|  global axiom directly. Does this compose well? I think so; you'll just
|  have to inline all of the coercions. But, the coercions won't ever get
|  too big, as they will always mirror exactly the structure of the types
|  being coerced. Simon, this is the sort of "magic" I was thinking of,
|  magical because I can't imagine a way this could be produced from an
|  HsExpr.
|  
|  Also, nice example of how the one-parameter design might aid the
|  programmer. 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.
|  
|  Richard
|  
|  On 2013-07-23 08:21, Joachim Breitner wrote:
|  > 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 allows nice error messages to be reported at
|  >> the site of a user's "deriving instance IsNT ...".
|  >
|  > My plan was to make all checks (constructors in scope; IsNT classes for
|  > all data constructor arguments present) in TcDeriv, so you get nice
|  > error messages. If it turns out that the actual coercion can only be
|  > generated in a later pass, then it the checks just need to be strong
|  > enough to make that pass always succeed.
|  >
|  >> - 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.
|  >
|  > I know; I was just using them until representational equality is in and
|  > plan to switch then.
|  >
|  >>  (Nominal coercions correspond to the "C" coercions from this paper)
|  >
|  > I got confused by C and T in my previous mails. In any case, I am only
|  > concerned with representational equality (T, it seems) for this
|  > project.
|  >
|  >> Or, it's possible
|  >> that we could add abstraction over representational coercions, but I
|  >> prefer the magical approach, because I don't see a general need for
|  >> the
|  >> ability to abstract.
|  >
|  > Hmm, I must admit I was assuming that once the roles implementation is
|  > in there will be ~# and ~#/T (or ~R#, which is a less-easy-to-confuse
|  > moniker) available in Core.
|  >
|  >
|  >> Now that I think of it, you may need to generalize the deriving
|  >> mechanism a bit. All current "deriving"s generate code that the user
|  >> could write. (Typeable is something of an exception here.) Here, the
|  >> generated code is something that a user can not write. Maybe that's
|  >> why
|  >> you wanted CoreExprs in the first place!
|  >
|  > Exactly. But it is also the reason why we are aiming for deriving
|  > classes (and not NT values), because it is already an established way
|  > of
|  > having the compiler generate code for you.
|  >
|  >
|  >> - I prefer the two-parameter class over a one-parameter, as it seems
|  >> more flexible.
|  >
|  > Thanks for spotting the phantom type replacing example, which is a
|  > features I’d also like to have. The type family was just a quick idea
|  > (and it would be neat to be able to ask GHCi via ":kind! (Concrete t)"
|  > what t looks like with all newtypes unfolded), but it’s not worth the
|  > loss of flexibility.
|  >
|  >
|  > In some cases, the type family might require less type annotations.
|  > Consider
|  > newtype Age = Age Int
|  > newtype NT1 = NT1 Int
|  > newtype NT2 = NT2 Int
|  >
|  > myCast :: Either NT1 Age -> Either NT2 Age
|  > myCast = castNT . uncastNT
|  >
|  > With two parameters, GHC will not know whether it should cast via
|  > "Either Int Age" or "Either Int Int", while with a type family there
|  > will be only one choice, "Concrete (Either NT1 Age) = Either Int Int".
|  > In general, castNT . uncastNT would have the nice type
|  >         castNT . uncastNT  :: Concrete a ~ Concrete b => a -> b
|  > which plainly expresses „Cast between any to values who have the same
|  > concrete representation.“. Just as a side remark in case this comes up
|  > later again.
|  >
|  >
|  >
|  > BTW, what should the base-case be? I believe most user-friendly is a
|  > least-specific class
|  >         instance IsNT a a
|  > so that the cast "Either Age a -> Either Int a" is possible. Or are
|  > overlapping instances too bad and the user should derive instances for
|  > all non-container non-newtype types himself:
|  >         instance IsNT Int Int ....
|  >
|  >
|  > Am Dienstag, den 23.07.2013, 05:23 +0000 schrieb Simon Peyton-Jones:
|  >> The question of how to represent all this in HsSyn, to communicate
|  >> between TcDeriv and TcInstDcls, is a somewhat separate matter.  We can
|  >> solve that in several ways.  But first we need be sure what the FC
|  >> story is.
|  >
|  > For now what I am doing is that in TcDeriv, I am implementing the
|  > method
|  > with a value "unfinishedNTInstance :: a" which I am then replacing in a
|  > always-run simplCore pass with the real implementation in Core. It is a
|  > work-around that lets me explore the design-space and implementation
|  > issues without having to rewire GHC.
|  >
|  > Greetings,
|  > Joachim
|  >
|  >
|  > _______________________________________________
|  > ghc-devs mailing list
|  > ghc-devs <at> haskell.org
|  > http://www.haskell.org/mailman/listinfo/ghc-devs

|  
|  _______________________________________________
|  ghc-devs mailing list
|  ghc-devs <at> haskell.org
|  http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
ghc-devs <at> haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs
Joachim Breitner | 4 Jul 01:06 2013
Picon

Re: Exposing newtype coercions to Haskell

Hi again,

Am Mittwoch, den 03.07.2013, 10:01 +0200 schrieb Joachim Breitner:
> Am Dienstag, den 02.07.2013, 16:28 +0000 schrieb Simon Peyton-Jones:
> > | I also noticed a problem with my logic for creating the NT-lifting
> > | function.  Suppose
> > |   data C a = MkC (Foo a)
> > | 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
> > | constructor, eg
> > |         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)
> > 
> > Dually, suppose Foo was an *abstract* type, where we can't see the constructors of Foo.  But the
programmer as exported fooNT :: NT a b -> NT (Foo a) (Foo b).  Then we *do* want to be able to derive
> > 	cNT :: NT a b -> NT (C a) (C b)
> > Instead maybe we say
> > 	deriving cNT :: NT a b -> NT (C a) (C b) using( fooNT )
> > listing the imported witnesses that we use.  Or maybe we say simply
> > 	deriving cNT :: NT a b -> NT (C a) (C b) 
> > and magically use any NT-typed things that are in scope.
> 
> Is this really the compiler’s job here? After all, the programmer would
> be able to write
> 
>         deriving cNT' :: NT (Foo a) (Foo b) -> NT (C a) (C b)
>         cNT :: NT a b -> NT (C a) (C b)
>         cNT = cNT' . fooNT
> 
> and expose just cNT to his users, so no expressiveness is lost by not
> providing automatic support here.

Hmm, I notice that this is not fully thought through. A problem is that
on the one hand, the operations we have on newtypes (which allow us to
lift coercions between the _type_ constructor parameters) suggest that
we want
        cNT :: NT a b -> NT (C a) (C b)
while the “do it by hand” intuition suggests that
        cNT :: NT (Foo a) (Foo b) -> NT (C a) (C b)
should be provided. But I only now notice that this function will not be
easily implemented. I guess in this case it could be using NthCo to get
a ~ b from Foo a ~ Foo b, but this is probably shaky.

This tension between the type constructor oriented coercions and data
constructor oriented policy needs a bit more thought.

Greetings,
Joachim

--

-- 
Joachim “nomeata” Breitner
  mail <at> joachim-breitner.de • http://www.joachim-breitner.de/
  Jabber: nomeata <at> joachim-breitner.de  • GPG-Key: 0x4743206C
  Debian Developer: nomeata <at> debian.org
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Nicolas Frisby | 2 Jul 19:56 2013
Picon

Re: Exposing newtype coercions to Haskell

This is an exciting effort! Just a quick reaction to Simon's comments on CoreM.

On Tue, Jul 2, 2013 at 9:11 AM, Simon Peyton-Jones <simonpj <at> microsoft.com> wrote:

To your questions:

·        To do these kind of things, CoreM will need more reader stuff.  In particular:

o   The global TypeEnv

o   The GlobalRdrEnv

For my light experimentation, I have recovered these two values from the ModGuts that all plugins receive. Hopefully someone will shout out if there's pitfalls to avoid.

  * The mg_rdr_env field is of type GlobalRdrEnv.

  * compiler/main/GHC.hs defines a function compileCore with a local definition that rebuilds a TypeEnv. I extracted this:

> \guts -> HscTypes.typeEnvFromEntities (CoreSyn.bindersOfBinds (mg_binds guts))
>                                            (mg_tcs guts)
>                                            (mg_fam_insts guts)

and it has worked so far.

HTH and good luck!
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Joachim Breitner | 3 Jul 12:33 2013
Picon

Re: Exposing newtype coercions to Haskell

Hi,

Am Dienstag, den 02.07.2013, 12:56 -0500 schrieb Nicolas Frisby:

> For my light experimentation, I have recovered these two values from
> the ModGuts that all plugins receive. Hopefully someone will shout out
> if there's pitfalls to avoid.
>
>   * The mg_rdr_env field is of type GlobalRdrEnv.

strange, why did I miss that?

But I can’t get it to work, even looking up an element that I took from
the GRE itself returns []:

    let e' = head (head (occEnvElts env))
    putMsgS $ showSDoc dflags (ppr e')
    putMsgS $ showSDoc dflags (ppr (lookupGRE_RdrName (nameRdrName (gre_name e')) env))

prints:

        GHC.NT.Type.NT
          imported from `GHC.NT.Type' at GHC/NT.hs:5:1-18
          (and originally defined at GHC/NT/Type.hs:6:6-7)
        []

Also, trying to construct a RdrName that I can look up fails:

    let rdrName = mkRdrQual (mkModuleName "GHC.NT.Type") (mkTcOcc "NT")
    putMsgS $ showSDoc dflags (ppr (lookupGRE_RdrName rdrName env))

prints also just [].

What am I doing wrong?

Thanks,
Joachim

--

-- 
Joachim “nomeata” Breitner
  mail <at> joachim-breitner.de • http://www.joachim-breitner.de/
  Jabber: nomeata <at> joachim-breitner.de  • GPG-Key: 0x4743206C
  Debian Developer: nomeata <at> debian.org
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Nicolas Frisby | 3 Jul 21:19 2013
Picon

Re: Exposing newtype coercions to Haskell

On Wed, Jul 3, 2013 at 5:33 AM, Joachim Breitner <mail <at> joachim-breitner.de> wrote:
[snip]

strange, why did I miss that?

But I can’t get [the GlobalRdrEnv lookup] to work, even looking up an element that I took from
the GRE itself returns []:

    let e' = head (head (occEnvElts env))
    putMsgS $ showSDoc dflags (ppr e')
    putMsgS $ showSDoc dflags (ppr (lookupGRE_RdrName (nameRdrName (gre_name e')) env))

prints:

        GHC.NT.Type.NT
          imported from `GHC.NT.Type' at GHC/NT.hs:5:1-18
          (and originally defined at GHC/NT/Type.hs:6:6-7)
        []

Also, trying to construct a RdrName that I can look up fails:

    let rdrName = mkRdrQual (mkModuleName "GHC.NT.Type") (mkTcOcc "NT")
    putMsgS $ showSDoc dflags (ppr (lookupGRE_RdrName rdrName env))

prints also just [].

What am I doing wrong?

Thanks,
Joachim

lookupGRE_RdrName looks something up in the environment and then prunes the results via `pickGREs`. I suspect your lookup is succeeding, but all of your results are getting pruned away.

> pickGREs :: RdrName -> [GlobalRdrElt] -> [GlobalRdrElt]
> -- ^ Take a list of GREs which have the right OccName                                                                                                 
> -- Pick those GREs that are suitable for this RdrName                                                                                                 
> -- And for those, keep only only the Provenances that are suitable                                                                                    
> -- *****Only used for Qual and Unqual, not Orig or Exact*****

Emphasis mine. NB that `nameRdrName` builds a RdrName via the Exact constructor. That's why your first attempt failed (I think).

Your second attempt fails for a sneakier reason, something I posted an email about a little while ago (cf "invoking front-end phases from within a GHC plugin?").

The GlobalRdrEnv is keyed on the getUnique result of an OccName. That unique is derived from the unique of the FastString contained in the OccName. The uniques of FastStrings are allocated linearly via a global variable. Unfortunately, your plugin image and the hosting compiler's image have distinct copies of this global variable, so FastStrings from your plugin do not get the same unique as the similar FastStrings that were used to build the GlobalRdrEnv's keys. Your plugin creates FastStrings when calling things like `mkTcOcc`, for example.

Unless we eventually include the FastStrings' global variable in the `CoreMonad.reinitializeGlobals` mechanism, I think the available workaround here is to filter `occEnvElts env` for gre_names where `occNameString` and `occNameSpace` match what you're looking for. Robustness may require also constraining the gre_prov field.

Good luck.
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Gmane