-
Notifications
You must be signed in to change notification settings - Fork 0
/
core-kinds.boba
74 lines (59 loc) · 2.81 KB
/
core-kinds.boba
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
about:
/// The kind of conrete data types that can be constructed at runtime.
kind Data : syntactic
about:
/// The kind of uniqueness and linear attributes on data types.
kind Sharing : boolean
about:
/// The kind of data types the are composed of a data component and a sharing component.
kind Value : syntactic
about:
/// The kind of constraints that can occur in the context of a function type at the top level.
kind Constraint : syntactic
about:
/// The kind of effect types, which can be optionally parameterized by values.
kind Effect : syntactic
about:
/// The kinds of labeled data types in structurally-typed records and variants.
kind Field : syntactic
about:
/// The kind of runtime permissions, part of the function attribute set.
kind Permission : syntactic
about:
/// The kind of totality and partiality attributes on function types.
kind Totality : boolean
about:
/// The kind of 'compile-time fixed size' types.
kind Fixed : abelian
about:
/// The kind of 'trusted data' attributes on strings and other data types.
kind Trust : boolean
about:
/// The kind of 'cleared for sharing' attributes on strings and other data types.
kind Clearance : boolean
about:
/// The function type in Boba carries a lot more information than just inputs and outputs.
/// It also tells what 'effects' it performs, what 'permissions' it requires from the context
/// it runs in, and whether or not the compiler believes it is 'total'. All three of these attributes
/// depend on the operations used within the body of the function, and can be inferred during
/// type inference.
type Function : {Effect} --> {Permission} --> Totality --> [Value] --> [Value] --> Data
about:
/// A tracked value is a data type with a sharing and validity annotation applied to it.
/// Since sharing analysis is so viral, value-kinded types end up being the arguments
/// required by most other types, since in Boba a data type without a sharing annotation
/// cannot be inhabited by any actual instance of a value.
type Tracked : Data --> Sharing --> Value
about:
/// Function types in Boba can be 'qualified' by a set of constraints. These constraints help
/// to drive type inference and allow a powerful form of ad-hoc polymorphism, similar to
/// Haskell's typeclass constraints. This constructor allows us to represent qualified types
/// as just another form of type, but these should really only occur as an outermost type
/// constructor since it doesn't make a lot of sense for constraints to be nested in types.
type Constrained : Constraint --> Value --> Value
about:
/// Since Boba supports a form of variable-arity polymorphism, we also need to have tuples
/// of constraints, which can be variable-arity. This allows for things like a generic
/// tuple equality function supporting variable arity polymorphism.
type ConstraintTuple : [Constraint] --> Constraint
export { * }