blob: 3618edfacd327c00b9878c11d4365b221bf6b33c (
plain)
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
|
Typestates
==========
Typestates could be implemented as a per-type state, that the type itself
can add or remove freely, but code outside it can only add/remove in a
restricted way.
There are different kinds of typestates, that could be useful for different
things.
* Temporary typestates:
- T = T'TS is disallowed (cannot be removed freely)
- T'TS = T is disallowed (cannot be added freely)
- example use cases:
- begin_*/end_* calls or similar, where end_* must be called.
- in multi-threading: locked lock
* Validation typestates:
- T = T'TS is allowed (can be removed, e.g. String Numeric -> String)
- T'S = S is disallowed (cannot be added freely)
Syntax
------
Which syntax to use? (String is the type, Numeric is the typestate)
String Numeric
String'Numeric
String:Numeric
String.Numeric
String[Numeric]
String(Numeric)
String#Numeric
String-NonNumbers
String+Numeric
String=Numeric
Numeric
NumericString
Numeric String # best?
Should it be allowed to combine typestates and generics?
Note: The first syntax (String Numeric) won't work with generics.
List String:Numeric
List String(Numeric)
List Numeric
List NumericString
List Numeric String
List of Numeric String
List Locked Lock
List of Locked Lock
Can it be combined with dependent types?
Can it be used to implement dependent types?
List (10) Numeric String
List (n) Numeric String
Length10 List Numeric String
Length (10) List Numeric String
|
