Can constraints be placed on type definitions?

[rsnikhil]

Is it possible to attach a constraint on a struct type definition?
For example the following is a structural view of a RISC-V virtual address:

struct VA_struct ('levels : Int, 'vpn_size : Int, 'log_pte_size : Int) = {
    vpns   : vector ('levels, dec, bits ('vpn_size)),
    offset : bits(12)
}

For example, an Sv32 VA has 2 VPNs of bits(10) type and 1 offset of bits(12) type, and PTEs (Page Table Entries) are 4 bytes (2^2). An Sv39 VA has 3 VPNs of bits(9) type and 1 offset of bits(12) type, and PTEs are 8 bytes (2^3).

In general, I'd like to add the constraint that the only legal parameter combinations are

(2, 10, 2)    (for the RV32 Sv32 virtual mem scheme)
(3,  9, 3)    (for the RV64 Sv39 virtual mem scheme)
(4,  9, 3)    (for the RV64 Sv48 virtual mem scheme)

One can of course place these constraints on the signature of any function that uses this type, but that would replicate it in every such function.

[Alasdair]

Technically yes, but I think it works the other way to how you are thinking. You can do:

struct VA_struct ('levels : Int, 'vpn_size : Int, 'log_pte_size : Int), 'levels >= 0 = ...

but this would make it a type error to use VA_struct anywhere 'levels < 0, rather than implicitly adding the constraint when the type appears. I would avoid adding constraints to types in general, and add them to functions using the types (as you would for typeclasses in Haskell for example).

If you have a complex constraint you can add a synonym like:

type valid_va_struct('levels : Int, 'vpn_size : Int, 'log_pte_size : Int) -> Bool = 'levels > 0 & ...

[rsnikhil]

I don't understand some of the comments:

but this would make it a type error to use VA_struct anywhere
'levels < 0, rather than implicitly adding the constraint when
the type appears.

But isn't this exactly what we want? I.e., a type error if 'levels < 0?

I would avoid adding constraints to types in general, and add them to functions using the types

But doesn't this replicate the constraint? I can see your ‘synonym' solution alleviates this, but it's still replication?

In particular, I see this constraint as a fundamental property of the
type, which should hold no matter where it's used.

[Alasdair]

What I meant was that:

type T('n), 'n >= 0 = int('n)

val foo : T('n) -> unit

is an error. Adding the constraint on the type forces it to be propagated to all functions using that type, so you must write:

type T('n), 'n >= 0 = int('n)

val foo : forall 'n, 'n >= 0. T('n) -> unit

instead.

[Alasdair]

If you want to have the constraints carried around with the type, you have to use existential quantifiers, like:

default Order dec

$include <prelude.sail>

struct VA_struct('levels, 'vpn_size) = {
    vpns   : vector('levels, dec, bits('vpn_size)),
    offset : bits(12)
}

type valid_va_struct('levels, 'vpn_size, 'pte_size) -> Bool =
  ('pte_size == 32 & 'levels == 2 & 'vpn_size == 10)
  | ('pte_size == 39 & 'levels == 3 & 'vpn_size == 9)
  | ('pte_size == 48 & 'levels == 4 & 'vpn_size == 9)

type VA('pte_size) = {'levels 'vpn_size, valid_va_struct('levels, 'vpn_size, 'pte_size). VA_struct('levels, 'vpn_size)}

function foo(vaddr : VA(39)) -> unit = {
    print_bits("offset = ", vaddr.offset)
}

val main : unit -> unit

function main() = {
    foo(struct { vpns = [0b000000000, 0b000000000, 0b000000000], offset = 0xFFF } : VA_struct(3, 9))
}

We don't have full type-inference, so you'll probably find a lot of places where type annotations become mandatory when adding these existential variables, i.e. here it won't type-check without the VA_struct(3, 9) annotation.

[rsnikhil]

Re. this:

     type T('n), 'n >= 0 = int('n)    // (Tdef1)

     val foo : T('n) -> unit          // (A)

is an error. Adding the constraint on the type forces it to be
propagated to all functions using that type, so you must write, instead:

     val foo : forall 'n, 'n >= 0. T('n) -> unit    // (B)

Ok, I tried it and, yes, indeed, I see (A) gives me a a type error:

     Could not prove constraints 'n >= 0 in type synonym int('n) with

but I don't understand the error.
I expected 'n >= 0 to now be implicitly a part of the definition of T('n).
Something's broken in my understanding of what types and type-checking mean here.

Suppose I had written, instead:

     type T('n) = int('n)       // (Tdef2)
     val foo : T('n) -> unit    // (A)

What is the difference between (Tdef1)(A) and (Tdef2)(A)?

I expected:

• For (Tdef1)(A): declaration (A) says that foo accepts any int('n) arg
• For (Tdef2)(A): declaration (A) says that foo accepts any int('n) arg where 'n >= 0

both of which seem sensible.
Clearly I'm confused, but I can't explain my way out of it.

[Alasdair]

If the declaration of a type has a constraint, then this constraint must be true for the type to be well-formed wherever it appears.

Because Tdef1 has a constraint, when T('n) appears in (A) we are required to prove the constraint in order for the type T('n) -> unit to be well-formed. The constraint on a type constructor works analogously to a forall constraint on a function call, like if you have:

val foo : forall 'n, 'n >= 0. int('n) -> unit

val bar : forall 'n. int('n) -> unit

function bar(x) = {
    foo(x) // does not typecheck as we can't prove 'n >= 0, so we would have to propagate this constraint
}

As I mentioned these constraints are not very useful, which is why I suggest just ignoring them in favour of constraints on functions.

[Alasdair]

More concretely for the Haskell example I mentioned earlier, the constraints on types in Sail work like Foo/bar below, and I think you are imagining they work like Baz/quux. The difference is whether the constraint appears on the left or the right of the datatype definition.

{-# LANGUAGE DatatypeContexts, ExistentialQuantification #-}

data Eq a => Foo a = Foo (Maybe a)

{- Fails to type check!
bar :: Foo a -> Maybe a
bar (Foo x) = x
-}

data Baz a = Eq a => Baz (Maybe a)

quux :: Baz a -> Maybe a
quux (Baz x) = x

[Alasdair]

Might be worth mentioning that Haskell will tell us "XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language"!

[rsnikhil]

More concretely for the Haskell example I mentioned earlier, the constraints on types in Sail work like Foo/bar below, and I think you are imagining they work like Baz/quux. The difference is whether the constraint appears on the left or the right of the datatype definition.

{-# LANGUAGE DatatypeContexts, ExistentialQuantification #-}

data Eq a => Foo a = Foo (Maybe a)

{- Fails to type check!
bar :: Foo a -> Maybe a
bar (Foo x) = x
-}

data Baz a = Eq a => Baz (Maybe a)

quux :: Baz a -> Maybe a
quux (Baz x) = x

Ah, ok. This example helps a lot. I think it identifies exactly what was confusing me. Thanks!