-
Notifications
You must be signed in to change notification settings - Fork 2
/
notes
116 lines (77 loc) · 3.1 KB
/
notes
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
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
##### 2017-03-02
Is allowing a Nat type actually useful?
If we want to allow subtraction of producer lengths, then Nat seems
more cumbersome than useful.
##### 2017-03-02
type-eval must return syntax, not literals, even for singletons,
otherwise, they wont work as types
##### 2017-03-02
Q: Should arith exprs have singleton types?
Current design decision: Yes
Yes:
- dont need to special case in ty-eval
- still need tyeval anyways?
- could move arith canonicalization to type rule?
- rule impl looks more awk in order to avoid looping
- ie, arith exprs and datums need explicit lifting
- see #%datum, +, -, etc...
No:
- wont be able to ty-eval vars
Q: This means some "types" will have singleton kinds,
ie, if an arith expr is written directly in a type, eg in fn sig.
Where to add the checking for this? separate fn or in typecheck?
Current design decition: Must be in typecheck, for rules that use "⇐ Int"
##### 2017-03-02
Q: Should tyvars have "type" (1) Int or (2) Nat?
Current design decision: Using (1) Int.
(1) Int
- allows doing subtraction, eg (Producer (- n m))
- must generate implicit constraint?,
eg, (define (f {n} [p : (Producer n)) -> (Producer (- n 1))))
- must produce constraint (>= (- n 1) 0)
(2) Nat
- subtraction disallowed
- can get away with not generating extra constraints?
##### 2017-03-01
Should type-eval be (1) a separate function or (2) integrated into the type rules?
Ie, (1) = normalize expanded types, (2) = normalize surface types
(2) implies "expansion = type-eval"?
I think (2) is the better approach.
It mostly works, BUT it's only useful if we only ever type-eval surface terms, which is not true.
E.g., (already-expanded) polymorphic types:
- after instantiation, we must type-eval again.
- re-expanding after instantiation won't trigger the normalizations
- solution? use the orig to instantiate?
- this is dangerous since relying on the binders in the orig may encounter the stxprop+binders problem
Falling back to (1).
##### 2017-02-28
Should types and kinds be (1) conflated or (2) distinct?
Current design decision: using (1)
(1) conflated
Pros: --------------------
- want to write rules like:
(define-typed-syntax blank
[(_ n) ≫
[⊢ n ≫ n- ⇐ Nat]
--------
[⊢ (v:#%app v:blank n-) ⇒ (Producer n)]])
and have it work for exprs like:
(blank (+ 1 2))
Ie, want to seamlessly lift expr n into type.
If there is a separate type constructor for addition, eg ty+ ,
then we need a more explicit lifting step which could be more awkward.
Cons: --------------------
- harder to use in define-typed-stx constructs
- ie, how to check type-wellformedness?
- must check for either ":: #%type"
- or ": Int"
- eg macro for Producer constructor is somewhat ugly
- Some arith types are arith exprs lifted to type level (see blank rule in Pros)
and some are directly written as types (eg fn signature).
The latter will have singleton type (see singleton type above),
so ty= must handle comparison between arith expr and type
- eg ty=? (+ 1 2) Int = ???
(2) distinct
Pros: --------------------
- easier to reason about?
Cons: --------------------