• Home
  • Line#
  • Scopes#
  • Navigate#
  • Raw
  • Download
1## Type system implementation
2
3Type system is simple: there are only parametric type families, named as `Sort`s, and their instances, named as `Type`s.
4
5For simplicity, all literals without parens are Sorts, with parens - Types.
6
7### Special types
8
9  - Bot() - subtype of all types, subtyping relation is made implicitly upon type creation.
10  - Top() - supertype of all types, subtyping rel is created implicitly.
11
12## Sorts
13
14Internally they denoted by indices (just numbers), and there is separate class to hold their names.
15For type_system description technical details can be ommited and Sorts will be understood in this
16text just as literals.
17
18## Types
19
20Internally they are just indices.
21
22A sort, acompanied with a list of parameters, becomes a type.
23
24Each parameter consists of: a sign of variance for calculating subtyping relation and a type.
25
26Variances are:
27- `~` invariant, means that corresponding parameter in subtyping relation must be in subtype and supertype relation
28      simultaneously
29- `+` covariant, means that suptyping relation of parameter is in direction of subtyping relation of type.
30- `-` contrvariant, direction of suptyping of parameter is in opposite to such of type.
31
32## Examples
33
34Sorts:
35
36- `i8`
37- `Math`
38- `function`
39
40Types:
41
42- `i8()`
43- `i16()`
44- `i32()`
45
46- `function(-i32(), -i16(), +i8())`
47- `function(-function(-i8(), +i16()), +i16())`
48
49Subtyping relations (`subtype <: supertype`):
50
51- `i8() <: i16() <: i32()`
52- `function(-i32(), -i16(), +i8()) <: function(-i16(), -i8(), +i32())`
53- `function(-function(-i8(), +i16()), +i16()) <: function(function(-16(), +8()), +i32())`
54
55## Closure
56
57After defining base types and initial subtyping realtion, a closure of subtyping relation is computed.
58This helps to speed up subtyping checking during verification.
59
60Loops in subtyping relation are threated as classes of equivalence, for instance:
61`a() <: b() <: c() <: a()` leads to indistinguishability of a(), b() and c() in type system.
62