Exposing newtype coercions to Haskell

Joachim Breitner mail at joachim-breitner.de
Thu Jul 11 10:41:22 CEST 2013


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.dehttp://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  • GPG-Key: 0x4743206C
  Debian Developer: nomeata at debian.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130711/25c61aff/attachment.pgp>


More information about the ghc-devs mailing list