The code below implements this approach. We use Scheme
notation for the source language (we could just as well supported ML
or Haskell-like notations). The notation for type terms is infix, with
the right-associative arrow. As an example, the end of the file
type-inference.scm shows the derivation for call/cc
, shift
and reset
from their types in the
continuation monad. Given the type:
(define (cont a r) `((,a -> . ,r) -> . ,r)) (((a -> . ,(cont 'b 'r)) -> . ,(cont 'b 'b)) -> . ,(cont 'a 'b))within 2 milli-seconds, we obtain the term for shift:
(lambda (_.0) (lambda (_.1) ((_.0 (lambda (_.2) (lambda (_.3) (_.3 (_.1 _.2))))) (lambda (_.4) _.4))))
From Curry-Howard correspondence, determining a term for a type is tantamount to proving a theorem -- in intuitionistic logic as far as our language is concerned. We formulate the proposition in types, for example:
(define (neg x) `(,x -> . F)) (,(neg '(a * b)) -> . ,(neg (neg `(,(neg 'a) + ,(neg 'b)))))This is one direction of the deMorgan law. In intuitionistic logic, deMorgan law is more involved:
NOT (A & B) == NOTNOT (NOT A | NOT B)The system gives us the corresponding term, the proof:
(lambda (_.0) (lambda (_.1) (_.1 (inl (lambda (_.2) (_.1 (inr (lambda (_.3) (_.0 (cons _.2 _.3))))))))))
The de-typechecker can also prove theorems in classical logic, via the double-negation (aka CPS) translation. We formulate a proposition:
(neg (neg `(,(neg 'a) + ,(neg (neg 'a)))))
and, within 403 ms, obtain its proof:
(lambda (_.0) (_.0 (inr (lambda (_.1) (_.0 (inl _.1))))))The proposition is the statement of the Law of Excluded Middle, in the double-negation translation.
Programming languages can help in the study of logic.
let
, sums and products -- and its
type. The code contains many comments that explain the notation, the
incremental composition of the typechecking relation and taking the
advantage of the first-class status of Kanren relations for
typechecking of polymorphic let
.logic.scm [9K]
Kanren code that illustrates the application of the inverse typechecker to proving theorems in intuitionistic and classical logics.
The Kanren project < http://kanren.sourceforge.net >
Deriving a program from its incomplete specification such as type using constraints, background knowledge, heuristics or training set is the subject of inductive programming
< http://www.inductive-programming.org >
int
. A type system is sound if it
correctly approximates the dynamic behavior and predicts its outcome:
if the static semantics predicts that a term has the type int
,
the dynamic evaluation of the term, if it terminates, will
yield an integer.
Conventional type-checking is big-step evaluation in the
abstract: to find a type of an expression, we fully `evaluate' its
immediate subterms to their types. We propose a different kind of type
checking that is small-step evaluation in the abstract: it unzips (pun
intended: cf. Huet's zipper) an expression into a context and a
redex. The type-checking algorithms in the paper are implemented in
Twelf; the complete code is available. In particular, the
well-commented file lfix-calc.elf
implements, by way of
introduction and comparison, small-step type-checking for simply typed
lambda calculus.
The benefit of small-step typechecking is that, by `following' the control flow, it is more suitable for effectful computations. A more interesting result comes from the fact that static evaluation, unlike the dynamic one, goes `under lambda'. Thus the small-step static evaluation context is a binding context.
Colon becomes the new turnstile! Since the evaluation context is neither commutative or associative but is subject to focusing rules, we obtain the framework for expressing various substructural and modal logics.
Joint work with Chung-chieh Shan.
small-step-typechecking.tar.gz [10K]
Commented Twelf code with small small-step typechecking algorithms and many sample derivations.
Abstract interpretation in the denotational context:
Patrick Cousot, Types as abstract interpretations. POPL 1997, 316-331.
Abstract interpretation as an aid during program development of logical programs:
Manuel Hermenegildo, Germa'n Puebla, and Francisco Bueno: Using global analysis, partial specifications, and an extensible assertion language for program validation and debugging.
In: The logic programming paradigm: A 25-year perspective, ed. Krzysztof R. Apt, Victor W. Marek, Mirek Truszczynski, and David S. Warren, 161-192, 1999. Berlin: Springer-Verlag.
Interpreting types as abstract values: A tutorial on Hindley-Milner type inference
gensyms
) a fresh type variable and watches for its
scope, following the proof rule for universal introduction. Due to
this implementation, rank-2 polymorphism has been used (some would say
abused) to express static capabilities and assure a wide variety of
safety properties statically, including:In each of these applications, the fresh types generated by the type checker seems to reflect fresh values generated by the program at run time. For example, when generating code as a first-order data structure, we need gensym not only at the type level to ensure lexical scope but also at the value level to make unique concrete variable names. Can dependent types expose and eliminate this reflection for the superfluous encoding that it is? In other words, can our code for generating fresh values be reused during type checking to assure their safety properties more directly? In particular, whereas generated types are only implicitly fresh and are equipped with no operations, generated values are explicitly fresh and are equipped with operations such as comparison. Can we use generated variable names to automate weakening?
Joint work with Chung-chieh Shan.
Lightweight Dependent-type Programming
Lightweight monadic regions
A few applications of fresh type variables, not counting the ST monad
oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML