-
Notifications
You must be signed in to change notification settings - Fork 5
Expand file tree
/
Copy pathtype-system.php
More file actions
226 lines (188 loc) · 7.71 KB
/
type-system.php
File metadata and controls
226 lines (188 loc) · 7.71 KB
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
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
<meta charset='utf-8' />
<meta name="viewport" content="width=device-width, initial-scale=0.6" />
<html>
<head>
<title>Type System - Plange</title>
<link rel=StyleSheet href='../css/general.css' type='text/css' />
</head>
<body>
<?php require('../header.php') ?>
<p>Types are used to constrain the structure and behavior (class invariant) of the values that a variable can be assigned, or that a constant can be defined as. Types may be eschewed, but benefit from static checks by the type system. Forgoing stack checks, use late binding, or duck typing. <a href="/documentation/syntax.php?name=TYPE_DEREFERENCE">Angle brackets</a> dereference types.</p>
<div class="code2">
<p>Declare and assign a variable.</p>
<pre>
<Int> x ← 10;
</pre>
</div>
<div class="code2">
<p>error caused by contradicting the invariant</p>
<pre>
<Int> x ← 10;
<b>x ← 1.5; //error - can't assign a fractional number to a variable of type Int</b>
</pre>
</div>
<p>Create types using the type keyword.</p>
<div class="code2">
<pre>
Color := type {
<Real> r;
<Real> g;
<Real> b;
};</pre>
</div>
<div class="code2">
<p>Reflection.</p>
<pre>
<Int> x;
print(type_of(x).name); //prints "Int"
print(type_of(Int).name); //prints "Type"
print(type_of(Type).name); //prints "Type"
print(typeof(type_of(Type).members)) // prints "Array<Meta.Member>"
</pre>
</div>
<p>Elide types where type constraints are undesired.</p>
<div class="code2">
<p>The identity function</p>
<pre>
identity := (value) { return value; };
</pre>
</div>
<h2>Type Constructors</h2>
<p>Parametric types are functions returning Type values, and syntactically identical to functions. These functions should be <a href="/documentation/syntax.php?name=TYPE_INVOCATION">invoked using the angle-bracket syntax</a>, which performs type checking.</p>
<div class="code2">
<p>Example</p>
<pre>
<Type * Int → Type> Vector := (T, s) { return T^s; }; // Vector is a function that returns a Type.
Float32x3 := Vector<Float32, 3>; // Create a concrete Type
<Float32x3> x; // a variable
<Vector<Float32, 3>> y; // all these variables are the same type
<type_of(x)> z; // contrived but doable
</pre>
</div>
<p>Despite the function-like definition, simple constructs (e.g. Vector from above) are recognized as parametric types and benefit from the generic features involving variance and deduction.</p>
<h3>Notes</h3>
<p>The angle-bracket syntax is not required, since parenthesis can be used also. The convention is to use the angle-bracket syntax when the intent is use as a parametric type (see <a href="/documentation/syntax.php?name=INVOCATION">INVOCATION</a>).</p>
<h2>Type inference</h2>
<p>Type inference, a feature of static typing, extends beyond inference of elided types in "obvious" scenarios, instead using all logical tools available (specifically constraint propogation and constant folding) for deduction. Type checking benefits from the same sophistication. Consider the following:</p>
<div class="code2">
<p>Example</p>
<pre>
getParamCount := (<Function<types, retType>> f) {
<List<Type>> types;
return types.length;
};
</pre>
</div>
<p><code>types</code> is never defined or assigned to, and is therefore unbound, but must be a List of Types. Upon attempting to evaluate <code>types.length</code>, a value for <code>types</code> is computed. An example of implicitly quantified generic programming:</p>
<div class="code2">
<p>Example</p>
<pre>
<(X * X → X) → Type> binary_op_type := (<X * X → X> f) { return X; }
</pre>
</div>
<p><code>X</code> is unbound, so may take on any type.</p>
<h2>Covariance and Contravariance</h2>
<p>The inheritance graph and variance properties are modeled and can be tested programmatically.</p>
<h3>Covariance</h3>
<div class="code2">
<p>Example</p>
<pre>
Animal := type {
<Void → Void> speak <- abstract;
};
Cat := type implementing Animal {
<Void → Void> speak <- { Meow(); };
};
<List<Animal> → Void> choir := (animals) {
for (animal in animals) {
animal.speak();
}
};
<Cat> bernard;
<Cat> russel;
List<Cat> kittehs := [ bernard, russel ];
choir(kittehs);
</pre>
</div>
<h3>Contravariance</h3>
<div class="code2">
<p>Example</p>
<pre>
<Animal → Void> solo := (animal) { animal.speak(); } ;
<Cat → Void> cat_solo = solo;
</pre>
</div>
<h3>Covariant method arguments</h3>
<p>Function overloads are ordered. The | operator, which is used to create function overloads, preserves the order of the elements (functions) and dispatches to the first overload that can accept the parameters.</p>
<div class="code2">
<p>Example</p>
<pre>
<Animal → Void> solo :=
(<Cat> _ ) { /* cats never do what you want */ } | // overload
(animal) { animal.speak(); }
;
</pre>
</div>
<p>Note that the semantics resemble pattern matching.</p>
<h2>Partial Types</h2>
<p>Types may be combined with the plus + operator to create a new type containing the elements from each. This operation is not associative, as the right hand side operator will override any elements from the left hand side.</p>
<div class="code2">
<p>Example (part 1 of 2)</p>
<pre>
SomeThing := type {
<String> data;
print_data := { print(data); };
} + DataProvider;
</pre>
<p>(part 2 of 2)</p>
<pre>
DataProvider := type {
<String> data := """
.,,uod8B8bou,,.
..,uod8BBBBBBBBBBBBBBBBRPFT?l!i:.
,=m8BBBBBBBBBBBBBBBRPFT?!||||||||||||||
!...:!TVBBBRPFT||||||||||!!^^""' ||||
!.......:!?|||||!!^^""' ||||
!.........|||| ||||
!.........|||| # ||||
!.........|||| ||||
!.........|||| ||||
!.........|||| ||||
!.........|||| ||||
`.........|||| ,||||
.;.......|||| _.-!!|||||
.,uodWBBBBb.....|||| _.-!!|||||||||!:'
!YBBBBBBBBBBBBBBb..!|||:..-!!|||||||!iof68BBBBBb....
!..YBBBBBBBBBBBBBBb!!||||||||!iof68BBBBBBRPFT?!:: `.
!....YBBBBBBBBBBBBBBbaaitf68BBBBBBRPFT?!::::::::: `.
!......YBBBBBBBBBBBBBBBBBBBRPFT?!::::::;:!^"`;::: `.
!........YBBBBBBBBBBRPFT?!::::::::::^''...::::::; iBBbo.
`..........YBRPFT?!::::::::::::::::::::::::;iof68bo. WBBBBbo.
`..........:::::::::::::::::::::::;iof688888888888b. `YBBBP^'
`........::::::::::::::::;iof688888888888888888888b. `
`......:::::::::;iof688888888888888888888888888888b.
`....:::;iof688888888888888888888888888888888899fT!
`..::!8888888888888888888888888888888899fT|!^"'
`' !!988888888888888888888888899fT|!^"'
`!!8888888888888888899fT|!^"'
`!988888888899fT|!^"'
`!9899fT|!^"'
`!^"'
""";
};
</pre>
</div>
<h2>Algebraic Types</h2>
<p>Types may be combined with the or | operator to create a new type thats instances must be any one of those types. This operator is associative.<p>
<div class="code2">
<p>Example</p>
<pre>
InteriorNode := type { <Int> value; <LinkedListNode> next; };
TerminalNode := type { <Int> value; };
LinkedListNode := InteriorNode | TerminalNode
</pre>
</div>
<p>Further, algebraic types are not limited to simple switching. Like all algebraic values, they may be defined through a system of constraints.</p>
<?php require('../footer.php') ?>
</body>
</html>