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
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
|
package examples
object typeinf {
trait Term {}
case class Var(x: String) extends Term {
override def toString() = x
}
case class Lam(x: String, e: Term) extends Term {
override def toString() = "(\\" + x + "." + e + ")"
}
case class App(f: Term, e: Term) extends Term {
override def toString() = "(" + f + " " + e + ")"
}
case class Let(x: String, e: Term, f: Term) extends Term {
override def toString() = "let " + x + " = " + e + " in " + f
}
sealed trait Type {}
case class Tyvar(a: String) extends Type {
override def toString() = a
}
case class Arrow(t1: Type, t2: Type) extends Type {
override def toString() = "(" + t1 + "->" + t2 + ")"
}
case class Tycon(k: String, ts: List[Type]) extends Type {
override def toString() =
k + (if (ts.isEmpty) "" else ts.mkString("[", ",", "]"))
}
object typeInfer {
private var n: Int = 0
def newTyvar(): Type = { n += 1; Tyvar("a" + n) }
trait Subst extends Function1[Type, Type] {
def lookup(x: Tyvar): Type
def apply(t: Type): Type = t match {
case tv @ Tyvar(a) => val u = lookup(tv); if (t == u) t else apply(u)
case Arrow(t1, t2) => Arrow(apply(t1), apply(t2))
case Tycon(k, ts) => Tycon(k, ts map apply)
}
def extend(x: Tyvar, t: Type) = new Subst {
def lookup(y: Tyvar): Type = if (x == y) t else Subst.this.lookup(y)
}
}
val emptySubst = new Subst { def lookup(t: Tyvar): Type = t }
case class TypeScheme(tyvars: List[Tyvar], tpe: Type) {
def newInstance: Type =
(emptySubst /: tyvars) ((s, tv) => s.extend(tv, newTyvar())) (tpe)
}
type Env = List[Pair[String, TypeScheme]]
def lookup(env: Env, x: String): TypeScheme = env match {
case List() => null
case Pair(y, t) :: env1 => if (x == y) t else lookup(env1, x)
}
def gen(env: Env, t: Type): TypeScheme =
TypeScheme(tyvars(t) diff tyvars(env), t)
def tyvars(t: Type): List[Tyvar] = t match {
case tv @ Tyvar(a) => List(tv)
case Arrow(t1, t2) => tyvars(t1) union tyvars(t2)
case Tycon(k, ts) => (List[Tyvar]() /: ts) ((tvs, t) => tvs union tyvars(t))
}
def tyvars(ts: TypeScheme): List[Tyvar] =
tyvars(ts.tpe) diff ts.tyvars;
def tyvars(env: Env): List[Tyvar] =
(List[Tyvar]() /: env) ((tvs, nt) => tvs union tyvars(nt._2))
def mgu(t: Type, u: Type, s: Subst): Subst = Pair(s(t), s(u)) match {
case Pair(Tyvar(a), Tyvar(b)) if (a == b) =>
s
case Pair(Tyvar(a), _) if !(tyvars(u) contains a) =>
s.extend(Tyvar(a), u)
case Pair(_, Tyvar(a)) =>
mgu(u, t, s)
case Pair(Arrow(t1, t2), Arrow(u1, u2)) =>
mgu(t1, u1, mgu(t2, u2, s))
case Pair(Tycon(k1, ts), Tycon(k2, us)) if (k1 == k2) =>
(s /: (ts zip us)) ((s, tu) => mgu(tu._1, tu._2, s))
case _ =>
throw new TypeError("cannot unify " + s(t) + " with " + s(u))
}
case class TypeError(s: String) extends Exception(s) {}
def tp(env: Env, e: Term, t: Type, s: Subst): Subst = {
current = e
e match {
case Var(x) =>
val u = lookup(env, x)
if (u == null) throw new TypeError("undefined: " + x)
else mgu(u.newInstance, t, s)
case Lam(x, e1) =>
val a, b = newTyvar()
val s1 = mgu(t, Arrow(a, b), s)
val env1 = Pair(x, TypeScheme(List(), a)) :: env
tp(env1, e1, b, s1)
case App(e1, e2) =>
val a = newTyvar()
val s1 = tp(env, e1, Arrow(a, t), s)
tp(env, e2, a, s1)
case Let(x, e1, e2) =>
val a = newTyvar()
val s1 = tp(env, e1, a, s)
tp(Pair(x, gen(env, s1(a))) :: env, e2, t, s1)
}
}
var current: Term = null
def typeOf(env: Env, e: Term): Type = {
val a = newTyvar()
tp(env, e, a, emptySubst)(a)
}
}
object predefined {
val booleanType = Tycon("Boolean", List())
val intType = Tycon("Int", List())
def listType(t: Type) = Tycon("List", List(t))
private def gen(t: Type): typeInfer.TypeScheme = typeInfer.gen(List(), t)
private val a = typeInfer.newTyvar()
val env = List(
/*
Pair("true", gen(booleanType)),
Pair("false", gen(booleanType)),
Pair("if", gen(Arrow(booleanType, Arrow(a, Arrow(a, a))))),
Pair("zero", gen(intType)),
Pair("succ", gen(Arrow(intType, intType))),
Pair("nil", gen(listType(a))),
Pair("cons", gen(Arrow(a, Arrow(listType(a), listType(a))))),
Pair("isEmpty", gen(Arrow(listType(a), booleanType))),
Pair("head", gen(Arrow(listType(a), a))),
Pair("tail", gen(Arrow(listType(a), listType(a)))),
*/
Pair("fix", gen(Arrow(Arrow(a, a), a)))
)
}
trait MiniMLParsers extends CharParsers {
/** whitespace */
def whitespace = rep{chr(' ') ||| chr('\t') ||| chr('\n')}
/** A given character, possible preceded by whitespace */
def wschr(ch: char) = whitespace &&& chr(ch)
def isLetter = (c: char) => Character.isLetter(c)
def isLetterOrDigit: char => boolean = Character.isLetterOrDigit
/** identifiers or keywords */
def id: Parser[String] =
for (
c: char <- rep(chr(' ')) &&& chr(isLetter);
cs: List[char] <- rep(chr(isLetterOrDigit))
) yield (c :: cs).mkString("", "", "")
/** Non-keyword identifiers */
def ident: Parser[String] =
for (s <- id if s != "let" && s != "in") yield s
/** term = '\' ident '.' term | term1 {term1} | let ident "=" term in term */
def term: Parser[Term] = (
( for (
_ <- wschr('\\');
x <- ident;
_ <- wschr('.');
t <- term)
yield Lam(x, t): Term )
|||
( for (
letid <- id if letid == "let";
x <- ident;
_ <- wschr('=');
t <- term;
inid <- id; if inid == "in";
c <- term)
yield Let(x, t, c) )
|||
( for (
t <- term1;
ts <- rep(term1))
yield (t /: ts)((f, arg) => App(f, arg)) )
)
/** term1 = ident | '(' term ')' */
def term1: Parser[Term] = (
( for (s <- ident)
yield Var(s): Term )
|||
( for (
_ <- wschr('(');
t <- term;
_ <- wschr(')'))
yield t )
)
/** all = term ';' */
def all: Parser[Term] =
for (
t <- term;
_ <- wschr(';'))
yield t
}
class ParseString(s: String) extends Parsers {
type inputType = int
val input = 0
def any = new Parser[char] {
def apply(in: int): Parser[char]#Result =
if (in < s.length()) Some(Pair(s charAt in, in + 1)) else None
}
}
def showType(e: Term): String =
try {
typeInfer.typeOf(predefined.env, e).toString()
}
catch {
case typeInfer.TypeError(msg) =>
"\n cannot type: " + typeInfer.current +
"\n reason: " + msg
}
def main(args: Array[String]) {
Console.println(
if (args.length == 1) {
val ps = new ParseString(args(0)) with MiniMLParsers
ps.all(ps.input) match {
case Some(Pair(term, _)) =>
"" + term + ": " + showType(term)
case None =>
"syntax error"
}
}
else
"usage: java examples.typeinf <expr-string>"
)
}
}
|
