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
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
|
Done:
- pattern match compiler prototípus
- beépítve a korábbi fordítóba
- IORef-es/STRef-es kiértékelő
-> ennek a használata elbonyolítaná az implementációt:
- mindent monadikussá kellene tenni, ez különösen fájdalmas mintaillesztéskor
- plusz típusváltozó minden típuban / vagy IO mindenhol
- explicit sharing mindenhol
- tiszta hatékony interpreter + típusellenőrző függő típusozáshoz
- tiszta, a Haskell lusta kiértékelését használja sharingre
- külön kiértékelő típusozás közben és típusozás után a hatékonyság növelésére
- type erasure a hatékonyság növelésére (az dep. type ellensúlyozására)
- memory leak ellen védett De Bruijn változók
- a kifejezésektől különválasztott típus a hatékonyság növelésére
- többszöri próbálkozás az beépítésre az előző fordítóba
még meglévő különbségek:
- nincs különválasztva a típusozás közbeni és utáni kiértékelés
- globális nevek vs. De Bruijn
- ad-hoc rejtett argumentumok (működnek vele a dep. rekordokkal emulált típusosztályok)
- ad-hoc RankNTypes (magic, valahogy működnek vele a dep. rekordokkal emulált típusosztályok)
- ad-hoc type erasure (megy konstruktorokra, nem megy a felhasználó által definiált kifejezésekre)
- nincs különválasztva a típus
- a kompozícionális típusozó nem tudja felhasználni a típusban megadott segítséget
- ez kizárja pl. RankNType-ot, és a függő típusozást
- a meglévő példákhoz nem kellett, összetettebb dep. rekordos típusosztályoknál kritikus lehet
- típusozó prototípus
- irányított (figyelembe veszi a megadott típusokat)
- dependens
- rejtett argumentumok
- RankNTypes
- pattern matching compiler beépítése
- több implementáció kipróbálása, a legutolsó zippereket használ
- könyebb debugolás
- eddigi leghatékonyabb
- kicsi implementáció, és bővíthetőnek is látszik
- címkézés a jobb mintaillesztés támogatáshoz
összefoglaló TODO lista
fő tennivaló: a típusozó kiegészítése
- syntactic sugars
- type classes as a syntax sugar
- egyszerűbb, átlátható szemantika
- könnyebb a más nyelvi elemekkel való viszonyát tisztázni
- modulárisabb implementáció
- könnyebben karbantartható
- könnyebben tesztelhető implementáció
- teljesítmény javítás, több check
-------------------------------------------------------------------------------- short-term TODOs
- recheck should not fail - coe missing?
- fix loop
primes
record02
recursivetexture01
- (a ~ b) + (a ~ c) ---> b ~ c (fragment06tailrecursion)
- row polymorphism
- swizzling
- record projection functions
- @ patterns
- hiding
-------------------------------------------------------------------------------- TODOs after 100% tests (completion & cleanup)
- dependent prelude should work again
- guards + where
- complete & review builtin reductions
- record filed name handling
- constructor operator fixities (also in patterns)
- data Wrong = Wrong a
- basic refactoring
- de-brunify move away from parser? / refactoring
- ambiguity check
- suppress univ. polymorphic ambiguity
- konstans megadott típus szigorúan vétele
- prohibit constraints like a ~ List a, a ~ a -> a, etc.
- bug fix (as needed)
- (~) :: forall a b . a -> b -> Type ?
- bug: head <-> tail csere nem jelez hibát, viszont recheck fails
- coe korrektebb használata (másmikor kell beszúrni) ?
- app típusozás jobban
-------------------------------------------------------------------------------- medium-term TODOs
- performance
- típus-érték különválasztás (vs. church style lambda)
- lam változó típusának kitörlése
expType
recheck
envDoc, expDoc
cstr
foldE ?
- neutrális termek külön
- konstruktorok univ. pol. típusainak kitörlése
- irrelevance + erasure
- max. De Bruijn index számolás
- ügyesebb De Bruijn (kitörlős)
- interpretált De Bruijn
- coe / type class irrelevance switch
- type classes
- generate type-case functions
- class parse + desugaring
- instance parse (drop it first)
- type class desugaring
- super class "visszaállítás"
- Constraint type: uniqueness of witnesses 0-1 elemű típusokra
- injektivitás inferencia
- open functions, type families syntax
- jobb hibaüzenetek
- jobb normalizáció elkerülés (String => [Char] lehetőleg ne)
- location infó
- kompozícionálisabb inference?
- dep. pattern matching
- evalXXX deriválás
- frekvenciák
- separate LambdaCube 3D specific parts
-------------------------------------------------------------------------------- cleanup after medium-term TODOs
- huge refactoring, documentation, test cases, ...
milestone: 1.0 compiler
-------------------------------------------------------------------------------- notes
--------------------------------------------------------------------------------
-------------------------------------------------------------------------------- row polymorphism
builtins
Split :: Type -> Type -> Type -> Constraint --Type
data RecordC (xs :: List (Pair String Type))
= RecordCons (tuptype (map snd xs))
tuptype [] = ()
tuptype (x: xs) = (x, tuptype xs)
Record :: List (Pair String Type) -> Type
Record xs = RecordC (sortBy fst xs)
builtins
project :: forall (xs :: List [(String, Type)]) . (s :: String) -> (Split (RecordC xs) (RecordC [(s, a)] b) -> RecordC xs -> a
-- project = ...
w :: Split a b c
iff
a = Record as
b = Record bs
c = Record cs
bs `sublist` as
cs `sublist` as
map fst bs `disjunct` map fst cs
:: Record {x: Float}
v1 :: Record {x: Float, y: Float, z: Float}
v1 = {x: 1.0, y: 2.0, z: 3.0} ----> RecordCons @[("x", _), ("y", _), ("z", _)] (1.0, (2.0, (3.0, ())))
v2 = {x: 1.0, y: 2.0, z: 3.0, a: 4.0}
f :: (Split a (Record {x: Float, y: Float}) b) => a -> Float
f v = v.x +! v.y
r = f v1 +! f v2 -- this is valid
exp.field -----> project field exp
f v1 -- a ~ Record {x: Float, y: Float, z: Float}
eval
Split (Record xs) (Record ys) c = eval $ c ~ Record (xs \\ ys)
Split (Record xs) c (Record ys) = eval $ c ~ Record (xs \\ ys)
Split a (Record xs) (Record ys) = eval $ a ~ Record (xs ++ ys)
|
