Opaque types?

[msaaltink]

I sometimes stub my toe by applying one of the built-ins, typically == or +, to something I shoudn't. The type-checker allows this because so many things satisfy Cmp (or is it Eq?) or Ring. So it would occasionally be convenient to have a type constructor that is not a member of these classes. For example, a constructor opaque with an interface like

wrap: {t} t -> opaque t
unwrap: {t} opaque t -> t

and where opaque t is in none of the type classes. It would be quite convenient if we also had the ability to write things like

f: opaque t -> ...
f (wrap x) = ...

There is a sort of a way to fake this now, for example, with

type opaque t =
  { payload: t
  , junk: [0]( Bit // eliminates Ring, Field, Round, Literal
             , () -> () // eliminates Eq, Cmp
             , Integer) // eliminats Logic
  }

unwrap: {t} opaque t -> t
unwrap x = x.payload

wrap: {t} t -> opaque t
wrap x = { payload = x, junk = []}

This does indeed prevent the inadvertent application of a built-in. It is not really satisfactory, though, as it makes opaque t not a testable or provable type. For example, with type opaque Bit

property tertium_non_datur x =
  unwrap x == True \/ unwrap x == False

in Cryptol we find

Main> :l opaque.cry
Loading module Cryptol
Loading module Main
Main> :check
property tertium_non_datur 
The expression is not of a testable type.
Type: Main::opaque Bit -> Bit
Main> :prove
:prove tertium_non_datur
        Not a valid predicate type:
Main::opaque Bit -> Bit

So, having a built-in opaque type constructor would be a win here. To be sure this is just a mild suggestion, as the situation comes up infrequently, but it seems like an easy thing to add.

Of course if you do add this feature, someone would be sure to ask why we could not now define a way to add custom definitions for some class, for example, adding my own functions to be == and != for my opaque type.

[robdockins]

I hesitate to even mention this because we are strongly considering removing this feature, but we actually have had for some time now an experimental newtype feature that does essentially what you request here.

newtype Box a = { contents : a }

Main> let x = Box { contents = 11 : Integer }
Main> :t x
x : Box Integer
Main> let y = Box { contents = 42 : Integer }
Main> y
{contents = 42}
Main> x+y

[error] at <interactive>:1:1--1:4:
  Unsolved constraints:
    • Ring (Box Integer)
        arising from
        use of expression (+)
        at <interactive>:1:1--1:4
Main> x.contents + y.contents
53

As we can see from #912, people do indeed want the ability to implement new instances :-) That would really be a major new language feature.

[robdockins]

After thinking about this a bit, I'm of the opinion that we ought to add newtype as a fully-supported feature rather than removing it. I don't think very much work would be required to complete support for it. The translation to SAWCore can just erase newtypes, I think, so it should be pretty easy to get that level of support working, at least. @yav, @brianhuffman, any thoughts?

[yav]

I always liked the idea of having newtypes which is why I added it :-) So I am 👍

[brianhuffman]

Erasing newtypes when translating to SAW should work for now. (Although at some point in the future it might be nice to make SAW preserve all Cryptol typing information, so we will probably want to revisit this later.) So I'm fine with making newtype fully supported.

[robdockins]

Newtypes are now fully supported with the merge of #1015.