-
Notifications
You must be signed in to change notification settings - Fork 16
/
types.theory.txt
183 lines (147 loc) · 12.9 KB
/
types.theory.txt
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
TYPES
BY LANGUAGE ==> # +-----------------------------+------------+----------+----------+-------------+
# | LANGAGE | CHECKING | EXPLICIT | SAFETY | DEFINITION |
# +-----------------------------+------------+----------+----------+-------------+
# | ASM x86 | none | strong | unsafe | structural |
# | PHP | dynamic | weak | safe | none |
# | JavaScript | dynamic | weak | safe | duck |
# | Python | dynamic | strong | safe | duck |
# | Ruby | dynamic | strong | safe | duck |
# | Perl | dynamic | weak | safe | nominative |
# | C | static | weak | unsafe | nominative |
# | BASIC | static | weak | safe | nominative |
# | C++ | static | strong | unsafe | nominative |
# | C# | static | strong | middle | nominative |
# | Java | static | strong | safe | nominative |
# | FORTRAN | static | strong | safe | nominative |
# | Pascal | static | strong | safe | nominative |
# +-----------------------------+------------+----------+----------+-------------+
/=+===============================+=\
/ : : \
)==: DEFINITION :==(
\ :_______________________________: /
\=+===============================+=/
TYPE ==> #A type is a name associated with a data structure.
#Type identity is linked to the:
# - structure:
# - e.g. two names pointing to same structure are same type
# - type checking can be:
# - static, i.e. compile-time ("structural")
# - dynamic, i.e. run-time ("duck typing"): similar to generic programming "concepts"
# - structure can be thought as:
# - the binary representation
# - the behavior:
# - i.e. associated algorithms/operators/methods, their constraint and their complexity
# - state can either be manipulated imperatively (mutated) or functionally (i.e. returned as copy)
# - the value space, i.e. set of possible values
# - name ("nominative"):
# - e.g. two names pointing to same structure are different types
DEFINITION ==> #During variable definition, type must be:
# - explicit: "manifest typing"
# - implicit and decided:
# - compile-time: "implicit typing" / "type inference"
# - runtime: "latent typing"
ABSTRACT DATA TYPE (ADT) ==> #Data type without implementation specifics
#E.g. integers vs 32-bit binary numbers
PROBABLISTIC DATA TYPE ==> #Data type that uses randomness.
#This includes data types whose operations give an approximate result, e.g. Bloom filters.
PERSISTENT DATA TYPE ==> #See state doc
OPERATIONS ==> #Most common operations on types:
# - create/insert
# - read:
# - by key: access
# - by value: search
# - update
# - delete
/=+===============================+=\
/ : : \
)==: COMPOSITION :==(
\ :_______________________________: /
\=+===============================+=/
SIMPLE VS COMPOSITE ==> #Composite|compound|aggregate types are composed of other types, as opposed to simple|primitive types.
#Data structures are composite types associated with specific algorithms/operations.
UNION TYPE ==> #Type which can be any of several given types.
#Also called "sum type".
#At runtime, the current type can either be:
# - tagged, i.e. recorded:
# - allows for better type checking
# - also called "discriminated union"
# - untagged:
# - takes less space
#"Top" type / "variant" is union of all possible types:
# - often called "any" or just "object" (when all types derive from base type "object")
INTERSECTION TYPE ==> #Type which combines constraints and behavior of several given types.
#Is conceptually similar to multiple inheritance.
DEPENDENT TYPE ==> #Composite type where one of its member's type has a constraint based on another member's type.
#Examples:
# - [NUM, NUM2], where NUM2 > NUM
# - FUNC(NUM)->ARR, where ARR.length === NUM
/=+===============================+=\
/ : : \
)==: SAFETY :==(
\ :_______________________________: /
\=+===============================+=/
STRONG VS WEAK/LOOSE TYPING ==> #Vague terms describing how much types are being checked|restricted, especially compile-time.
#Includes type checking, type safety, duck typing, implicit|latent typing, etc.
TYPE SAFETY ==> #Robustness of a typing system.
#Includes type casting, type checking, memory safety, type punning, etc.
TYPE CHECKING ==> #Type checking is type conformity:
# - between argument and parameter, including operators and assignments
# - during type casting
#Can be done:
# - compile-time ("static")
# - more robust
# - more performant: not done runtime, and more optimizations
# - usually compiled languages
# - runtime ("dynamic")
# - more flexible (can create types runtime, simpler metaprogramming)
# - no compile-time required
# - usually scripted languages
# - both ("gradual typing")
MEMORY SAFETY ==> #Checking for problems like array overflow or wrong pointer dereferencing
TYPE CASTING ==> #Changing the type of a value.
TYPE PUNNING ==> #Low-level typecasting.
#E.g.:
# - retrieving sign bit of a float
# - C union typecasting, depending on machine-level byte-wise disposition
TYPE CHANGE ==> #If variables can change type during their lifetime, especially because of control flow,
#it is "flow-sensitive typing"
/=+===============================+=\
/ : : \
)==: RESOLUTION :==(
\ :_______________________________: /
\=+===============================+=/
NAME RESOLUTION ==> #Associating identifier with a value
#Can be according to (in order):
# - namespaces
# - scope (name binding)
# - polymorphism (dispatch)
#Tradeoff compile-time/runtime is between robust|performant and flexibility
NAME BINDING ==> #Scope resolution. Can be:
# - compile-time (static|early binding)
# - runtime (dynamic|late|virtual binding)
#Scope: environment (set of variables) available in a given block
#Depends on which context (current code position) is used:
# - static|lexical scoping:
# - uses lexical context (position in source code)
# - compile-time
# - e.g. in which block a function was defined
# - more modular (e.g. easier to isolate scopes)
# - dynamic scoping:
# - uses execution|runtime|calling context (position in call stack)
# - run-time
# - e.g. from which block a function was fired
# - more flexible
#Level (what "blocks" means):
# - expression, block, function, file, module, global
#Parent environment can be inherited:
# - by value or by reference
#Masking|shadowing:
# - when current scope override some variables from parent
DISPATCH ==> #Polymorphism resolution. Can be:
# - compile-time (static)
# - usually using name mangling (type information concatenated to function name)
# - runtime (dynamic)
# - usually using virtual table (hash of function pointers, resolved at runtime)