Programming contest: Type checker.

Task: Write a type checker and inference engine for this small statically typed language (parser and evaluator optional. You may enter the AST directly in the source code, and you only need to ensure that invalid programs are failed and valid ones are passed).


; def: (def symbol arguments code), (def symbol code) or (def symbol)
; ∀: (∀ (variables) ((constraints)) code) returns code
; ∷: (∷ symbol type) returns symbol, type-annotated.
; →: (→ type1 type2 … returnType) returns type
; #+: primitive + of type (→ Int Int Int)

(def (∷ + (→ Int Int)) (x) x)
(def (∀ (χ) ((∷ + (→ Int . χ))) (∷ + (→ Int Int . χ)))
    (x y . r) (+ (#+ x y) . r)))

; (+ 1 1 1) → 3
; (+ 1 1 1 1) → 4
; ((+ 1) 1) → 2 (the language is curried)

; Interface example, assume an IO monad, String, write and sprintf:
(def (∷ Writeable (∀ (χ) ((∷ write (→ χ String (IO ())))) χ)))
(def (∷ fprintf (∀ (χ α) ((∷ Writeable χ) (∷ sprintf (→ ,@α String))) (→ χ ,@α (IO ()))))
    (a . b) (write a (sprintf . b))
Everything type annotation except the interface example should be able to be inferred. Feel free to improve the syntax of types that now use unquote-splicing as long as the semantics are the same.

The winner will be decided on the 1st of January. Criterions will be code size, elegance, helpfulness of error messages, and speed.

2011
using sexp syntax instead of mlite for typed lambda calculi

laughingirls.jpg