guile-devel
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Parsing


From: Ian Grant
Subject: Re: Parsing
Date: Tue, 16 Sep 2014 20:10:50 -0400

On Mon, Sep 15, 2014 at 4:38 PM, Stefan Israelsson Tampe <address@hidden> wrote:
I have been wondering if one could speed proofs myself, and especially for type provers.

What do you mean by 'type provers'? Do you mean type inference? I did a purely functional implementation of Hindley-Milner type inference: http://prooftoys.org/ian-grant/hm/ and its performance is good. It can infer the types of pathalogical examples such as Mairson's, in less than a minute. This is a type _expression_ which takes 50,000 lines of output on a 80-column terminal:

let fun pair x y = fn z => z x y 
    val x1 = fn y => pair y y 
    val x2 = fn y => x1 (x1 y)
    val x3 = fn y => x2 (x2 y)
    val x4 = fn y => x3 (x3 y)
    val x5 = fn y => x4 (x4 y)
in
   x5 (fn z => z)
end


reply via email to

[Prev in Thread] Current Thread [Next in Thread]