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@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs
