previous   next   up   top

Types

 


 

Inverse typechecking and theorem proving in intuitionistic and classical logics

A logic programming system with first-class relations and the complete decision procedure (e.g., Kanren) can define the pure Hindley-Milner typechecking relation for a language with polymorphic let, sums and products. The typechecking relation relates a term and its type: given a term we obtain its type. It can also work in reverse: given a type, we can obtain terms that have this type. Or, we can give a term with blanks and a type with blanks, and ask the relation to fill in the blanks.

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.

Version
The current version is 1.2, Jan 26, 2006.
References
type-inference.scm [19K]
Kanren code for the pure Hindley-Milner type inference relation relating a term in the lambda-calculus with fixpoint, polymorphic 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 >

Reversing Haskell typechecker

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 >

 

Type checking as small-step abstract evaluation

We expound a view of type checking as evaluation with `abstract values'. Whereas dynamic semantics, evaluation, deals with (dynamic) values like 0, 1, etc., static semantics, type-checking, deals with approximations like 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.

Version
The current version is 1.1, June 2007.
References
A Substructural Type System for Delimited Continuations
This paper introduced small-step typechecking when designing the first sound type system for dynamic delimited continuations.

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

 

How to reify fresh type variables?

To type-check a use of rank-2 polymorphism, a type checker generates (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.

References
Chung-chieh Shan: talk at the Shonan meeting on dependently typed programming. Shonan Village Center, Japan. September 15, 2011.
< http://www.cs.rutgers.edu/~ccshan/metafx/shonan.pdf >

Lightweight Dependent-type Programming
Lightweight monadic regions
A few applications of fresh type variables, not counting the ST monad



Last updated February 7, 2014

This site's top page is http://okmij.org/ftp/

oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!

Converted from HSXML by HSXML->HTML