Commit c16366c8204feca55cae3277315d1cd963ae35da

  • avatar
  • Antti-Juhani Kaijanaho <antti-juhani @kaij…> (Committer)
  • Fri Nov 16 19:46:07 EET 2012
  • avatar
  • Antti-Juhani Kaijanaho <antti-juhani @kaij…> (Author)
  • Fri Nov 16 19:46:07 EET 2012

Signed-off-by: Antti-Juhani Kaijanaho <>
(37 / 0)
1This is a very simple interpreter for an extended lambda calculus.
2It does Hindley–Milner style type inference and graph reduction.
4Compile with:
5 yacc hm.y && gcc -std=c99 -pedantic -Wall -Wextra -O2 -o hm
7Programs in this language consist of zero or more global definitions
8interspersed freely with zero or more terms, each on its own line.
9The interpreter takes them in linear order, one at a time,
10typechecking each and either evaluating it(for terms) or storing it
11(for definitions). Evaluation gets printed out one step at a time.
13Global definitions have the form
15 <var> = <term>
17The definition is not recursive; any reference in the right-hand-side
18to a variable having the same name as the one being defined is taken
19to refer to a previous definition of that variable.
21Variable names start with a letter or the underscore and continue with
22zero or more alphanumeric characters and underscores.
24Terms are as in the untyped lambda calculus with extensions for
25integer constants, addition, pairs (with projection functions "fst"
26and "snd"), mu-forms and (nonrecursive) let-forms.
28Mu forms are used for expressing recursion: mu <var> . <term>
29expresses the equation <var> = <term> and evaluates to the solution of
30that equation.
32The type system is a straightforward Hindley-Milner inference engine.
33Types are generalized when variables are introduced in the environment
34by global definitions and let forms. No generalization is done for
35the formal parameters of lambda abstractions or mu forms.
37Examples can be found in the file unimaginatively called foo.