Use result type instead of `MemoryOpResult`, `TR_Result`, and `PTW_Result`

[Timmmm]

Sail has a standard result type in it's library now so we should replace these:

union PTW_Result('paddr : Type, 'pte : Type) = {
  PTW_Success: ('paddr, 'pte, 'paddr, nat, bool, ext_ptw),
  PTW_Failure: (PTW_Error, ext_ptw)
}

union TR_Result('paddr : Type, 'failure : Type) = {
  TR_Address : ('paddr, ext_ptw),
  TR_Failure : 'failure,
}

union MemoryOpResult ('a : Type) = {
  MemValue     : 'a,
  MemException : ExceptionType
}

with e.g:

type MemoryOpResult('a : Type) = result('a, ExceptionType)

[martinberger]

There is a minor issue here in that Sail's type abbreviations (like type MemoryOpResult('a : Type) = ...) are structural rather than nominal. This might be most easy to see with an example. This compiles

type Giraffe = unit
type Dolphin = unit

function giraffe_identity(g : Giraffe) -> Giraffe = { g }
function dolphin_identity(d : Dolphin) -> Dolphin = { giraffe_identity(d) }

but the typing system is probably not enforcing what the author of the abbreviations Giraffe and Dolphin had in mind. This is not a problem in most cases, especially with complex types, and indeed not in any of the examples above, but it's worth bearing in mind since it is not documented that Sail's type abbreviations are structural.

@Timmmm @Alasdair

[Alasdair]

Yes, type introduces synonyms for existing types rather than creating new ones. You could do:

newtype Giraffe = Giraffe : unit
newtype Dolphin = Dolphin : unit

à la Haskell

[martinberger]

NICE ... but how should we know that newtype exists?

Be that as it may, I think we should replace all occurrences of type by newtype (where that is possible) in the RISCV model to increase type safety. The model currently has a lot of aliases for e.g. unit and many bits(n) have aliases, e.g.

type vaddr32 = bits(32)
type pte32   = bits(32)

type pte64   = bits(64)
type pte48   = bits(64)

[Alasdair]

I don't have the same Haskell optimisation that guarantees newtype is zero-cost right now, and I think simple aliases for bit vector types are fine if it's just to increase self-documentation. It's also just another way to write a union with a single constructor, so it might be better to just use union, as I have since learned that copying Haskell-isms is not very intuitive for most people...

[martinberger]

Additional type safety is more important than a small performance loss. I think with a short explanation in the manual (which I would happily write) everybody gets the distinction. Most programmers have heard of the related concept of "duck typing". Using union OTOH ...

[Alasdair]

Yes, writing a union with a single element as a wrapper is a bit counter-intuitive. I suspect that's why rust over-loaded the struct keyword for this, rather than using its enum keyword.

struct New_type_wrapper(old_type);

even though it's the same as

enum New_type_wrapper { New_type_wrapper(old_type) };

[Timmmm]

Ah this is very timely, because I just fixed a bug where I mixed up physical and virtual addresses and was just thinking "if only I could do newtype physaddr = xlenbits; newtype virtaddr = xlenbits!

How come newtype isn't in the Grammar section of the manual? I kind of assumed that was autogenerated and therefore complete.

It's also just another way to write a union with a single constructor, so it might be better to just use union, as I have since learned that copying Haskell-isms is not very intuitive for most people...

I think I would definitely prefer newtype. It's an increasingly common idiom in "normal" programming languages, so I think it's definitely in the "non-Haskell programmers will understand this" category. E.g:

• https://doc.rust-lang.org/rust-by-example/generics/new_types.html
• https://docs.python.org/3/library/typing.html#newtype

[Alasdair]

The sed script I have for cleaning up the grammar is a bit over-zealous, which is why it isn't in the manual

[martinberger]

@Alasdair BTW what is the semantics of newtype constructors and destructors?

In particular, does Sail's newtype share Haskell's restriction to types with exactly one field inside it? I think the answer is yes, because

enum E1 = {A}
newtype E1_Alias = E1_Alias : E1

compiles, but this does not:

enum E2 = {B, C}
newtype E2_Alias = E2_Alias : E2

It might be nice to have unrestricted newtype.