Refinement types for Cogent

Tests for Refinement Type in Cogent

Cogent information:

• branch: wip-reftypes
• commit: 8e43ce3666331980a116ce9842584dbb77a4a1f0

NOTE: the following two programs are very different. The first one ends up with an addition with incompatible unsigned int types, whereas the latter one is valid. (This has nothing to do with ref.types though.)

-- should fail
foo : U8 -> U8
foo x = x + 256

-- should pass
foo : U8 -> U8
foo x = x + 255 + 1

As unsigned int under/over-flow is very widely used, well-behaved, well-understood among researchers and programmers, and formally specified, there’s no reason we reject under/over-flow. However, whenever desired, the user can use refinement types to check that it doesn’t happen, just as we all learn in first-year computing courses, that the result of an addition is larger than either argument.

array size restriction through if

The follwing code fails although it should pass. Maybe due to type normalization.

-- !!!! failed
-- should pass
-- the if branching is not added to SMT solver
bar : U32 -> U32
bar x = if x < 3   
        then [1,2,3,4] @ x
        else 0

But if we use refinement type to limit the array index, it will work:

type Lt3 = [x: U32 | x < 3]

-- passed
-- should pass
foo : Lt3 -> U32
foo x = [1,2,3,4] @ x

Neither this (with let) because it won’t apply if constraints.

-- !!!! failed
-- should pass
bar : U32 -> U32
bar x = if x < 3 then let y = x in [1,2,3,4] @ y else 0

But it works when the targeting output is refinement type.

type Lt4 = [x: U32 | x < 4]

-- passed
-- should pass
bar : U32 -> Lt4
bar x = if x < 3 then x + 1 else 0

dead code well-typedness

We require that even in unreachable branches, they are well-typed.

type Lt3 = [x: U32 | x < 3]

foo : Lt3 -> U8
foo x = if x >= 3 then False else x

record field initialization

Non-exhaustive pattern in cogent internal. Maybe due to type normalization.

type R = { f1 : U8, f2 : U8 }
type RR = [v : R | v.f1 < 10]

-- !!!! failed
-- should pass
foo : RR -> RR
foo (r {f1, f2}) = r {f1, f2}

temporary value refinement

In the following case, the compilation will fail as expected.

f1: U8 -> [v: U8 | v < 10]
f2: U8 -> [v: U8 | v < 2]

-- failed
-- should fail
bar : U8 -> [v: U8 | v > 100]
bar x = let y = f1 x and z = f2 x in y + z

However, if we don’t use any temporary variable to store the result, the SMT solving phase will fail.

f1: U8 -> [v: U8 | v < 10]
f1 x = 1

f2: U8 -> [v: U8 | v < 2]
f2 x = 1

-- !!!! failed
-- this example failed at SMT solver but not type checker
bar : U8 -> [v: U8 | v > 100]
bar x = let y = f1 x in (f2 x) + y

large array

The max range of unsigned 32 is 4,294,967,295, (array size should +1) thefore a U32 could fetch array with this size without limitation.

-- !!!! failed
-- should pass
foo : (U8[4294967296]!, U32) -> U8
foo (x, y) = x @ y

If we set refinement range equal to 4,294,967,296, it could infer the number to be U64.

-- failed
-- should fail (4294967296 is U64, different in base type)
type R32 = [v: U64 | v <= 4294967296]

We cannot retrieve array by index in unsigned 64.

type R64 = [v: U64 | v < 4294967296]

-- !!!! failed
-- should pass
foo : (U8[4294967296] !, R64) -> U8
foo (x, y) = x @ y

Unless we explicitly specify the range of refinement type, the checker cannot infer the range of U32.

dependent record field

Not sopported yet.

type R = { f1 : U8, f2 : U8 }
type RR = [v : R | v.f1 < v.f2]

-- !!!! passed
-- should fail
foo : RR -> RR
foo (r {f1, f2}) = let x = r {f1 = f2} in x {f2 = f2}

type R = { f1 : U8, f2 : U8 }
type RR = [v : R | v.f1 < v.f2]

-- !!!! passed
-- should fail
foo : RR -> RR
foo (r {f1}) = r {f1 = 100}