Newtype coercions

[Stefan Höck]

Dear all

In Idris2, is it possible to proof that a value wrapped in a
newtype-like data wrapper still has the same runtime
representation? For instance, it would be useful to have

```
UnwrapId : a = Identity a
UnwrapId = ?foo

unIdList : List (Identity a) -> List a
unIdList xs = rewrite (cong List (UnwrapId {a = a})) in xs
```

If I understand correctly, this would coerce the given list without any
runtime cost (similar to `coerce` in Haskell).

Is this possible in Idris and if not, is it safe to implement `UnwrapId`
by using `believe_me` or do we need an interface similar to `Coercible`
in Haskell for this?

Thanks

Stefan

[Leif Warner]

I believe believe_me should be safe for this.

Just trying on this, it seems to work fine:

data Wrap a = MkWrap a

x : Int
x = 123

wrapped : Wrap Int
wrapped = MkWrap x

z : Int
z = believe_me wrapped

main : IO ()
main = printLn z

--
You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/20210121075110.GA14901%40ruehli-laptop.

[Stefan Höck]

Hi Leif

Thanks for your quick reply. I am wondering, though, whether this is
guaranteed to be safe across backends. Also, I'd feel better (and safer) if
this kind of guarantees could be provided by the typechecker.

For instance, assume somebody changed the implementation of `Identity`,
for instance by annotating it with `noNewtype`, the call to `believe_me`
would now introduce a potential bug.

> To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/CAG2mRG5fV3KC1QjmNr64usv8OkedpQmVU%3Dyw%2BZRO5NmRJ1dCag%40mail.gmail.com.

[Matus Tejiscak]

On Thu, Jan 21, 2021 at 11:50:01AM +0100, Stefan Höck wrote:
> Thanks for your quick reply. I am wondering, though, whether this is
> guaranteed to be safe across backends.

I'd say it is. The newtype optimisation is applied during translation to
CExp. Existing backends generate code from CExp or its further
simplifications.

In theory, you could imagine a backend that would work from TT instead
of CExp, where the newtype optimisation would not apply. Despite being
technically possible, I don't think that's the intended way of writing

backends.

> Also, I'd feel better (and safer) if this kind of guarantees could be
> provided by the typechecker.

Sadly, as far as I know, Idris has currently no means to talk about (the
equivalence of) the runtime representation of things.

How would you encode such information/knowledge in the type system?
Using some sort of Coercible typeclass? It would be an interesting thing
to figure out how the compiler could autogenerate instances depending on
the optimisations done on the IR...

> For instance, assume somebody changed the implementation of
> `Identity`, for instance by annotating it with `noNewtype`, the call
> to `believe_me` would now introduce a potential bug.

Indeed, believe_me is highly unsafe and should not be used ordinarily.
If we want to model the equivalence of runtime representation, we should
come up with something else that wraps believe_me safely (or replaces
it) for that particular purpose.

Matus

[Stefan Höck]

Hi Matus

Thank you very much for your replay.

Theoretically we could verify this particular optimization for newtypes using
Elaborator Reflection (and therefore of course also during compilation):
Checking, whether a data type consists of a single
constructor wrapping a single value and is not annotated with
`noNewtype` should be doable.

We could then define an interface `Coercible` (similar to the one found
in Haskell) and provide a macro for implementing its `coerce` function.
However, in Haskell it does not stop there. There is also a system for
annotating type parameters with a 'role' since it is not desirable to
allow the coercion of values in all cases even if they do have the same
runtime representation.

Consider for instance a sorted map data type `Map k v` that sorts its
keys according to an `Ord` instance. If such a Map is coerced to a
different key type of the same runtime representation but with a
different `Ord` instance, this would invalidate the Map's invariants.

Here is a [link](https://gitlab.haskell.org/ghc/ghc/-/wikis/roles) about
roles in Haskell, and here a
[library](https://hackage.haskell.org/package/no-role-annots-1.1/docs/Language-Haskell-RoleAnnots.html)
about defining role annotations through a typeclass instead of via
a compiler extension. If I find the time, I'll do some experiments
along the way of library 'no-role-annots'. However, the topic seems to
be quite involved, so it might require some serious considerations to
make sure that the optimizations are indeed safe.

Regards

Stefan

> --
> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/YAmbBbnPxEu9Xv2V%40localhost.