* Am 21.07.06 schrieb Joel Wright:
> Hi Everyone,
>
> It is my pleasure to announce the immediate availability of a
> Functional Pearl entitled "A type-correct, stack-safe, provably
> correct, expression compiler in Epigram", which will shortly be
> submitted to the Journal of Functional Programming.
>
> The abstract is included below, and the full paper and program source
> can be found at "http://www.cs.nott.ac.uk/~jjw"; (also on
> "http://www.e-pig.org/"; soon).
>
> We hope you enjoy it,
> Joel Wright and James McKinna.
>
> ----------------
> --- ABSTRACT ---
> ----------------
>
> Conventional approaches to compiler correctness, type safety and type
> preservation have focused on off-line proofs, either on paper or
> formalised with a machine, of existing compilation schemes with
> respect to a reference operational semantics. This pearl shows how the
> use of dependent types in programming, illustrated here in Epigram,
> allows us not only to build-in these properties, but to write programs
> which guarantee them by design and subsequent construction.
>
> We focus here on a very simple expression language, compiled into
> tree-structured code for a simple stack machine. Our purpose here is
> not to claim any sophistication in the source language being modelled,
> but to show off the metalanguage as a tool for writing programs for
> which the type preservation and progress theorems are self-evident by
> construction, and finally, whose correctness can be proved directly in
> the system.
>
> In this simple setting we achieve the following;
>
> * a type-preserving evaluation semantics, which takes a typed
> expression to a typed value.
> * a compiler, which takes a typed expression to stack-safe
> intermediate code.
> * an interpreter for compiled code, which takes stack-safe
> intermediate code to a big-step stack transition.
> * a compiler correctness proof, described via a function whose
> type expresses the equational correctness property.
Hi Joel,
i only had a short glimpse on your paper yet: seems like it's your
careful design of the intermediate code which allows you to elegantly
show that the 'McCarthy-Painter diagram' commutes. -
Hope you don't mind me clinging on an issue which is slightly off-topic
of your paper, but which naturally sticks out to me not just because you
address it in your concluding remarks.
At the moment, i lack a syntax-coloured imagination how your program
would look like without type tags. But concerning Epigram's conversion
rule not beeing able to type n : Nat as n : (Val T) i would like to
mention the following:
Type theory's ι-reduction exhibits a 'residuating' behaviour:
computations may get stuck on open terms. So you can't unify Nat with
Val T, because it's neither in head-normal form nor a variable. But if
some other computation were to bind T, you could come back and
either solve or refute this equation. Conor recently exemplified the
intricacies this brings on a Coq bug.
But instead of suspending a computation facing a free variable one could
also start 'guessing' possible values for it by unifying the application
with the call patterns of a functions definition.
Such a reduction strategy is called 'narrowing' and one of its drawbacks
is possible non-termination when applied to inductive datatypes: a
function defined on the naturals may eventually enumerate the infinite
many solutions for its input.
Moreover, to retain functionality when returning the inferred argument
one better makes sure to deal with one-to-one mappings only. You almost
can find an example of this in the 'Eliminating Dependent Pattern
Matching' paper by Goguen, McBride and McKinna.
http://www.cs.nott.ac.uk/~ctm/goguen.pdf
Where for a function
f : S -> T
a predicate of beeing an image under f is developed
Imf (t:T) : * = imf (s:S) : Imf (f s)
which allows for a value of the target type the call which leads to it
to be inferred
inv (t:T;p:Imf t) :S
inf (f s) (imf s) |-> s
Inverting a function is not possible in general, because it logically
corresponds by way of type scheming to Peircean abduction:
S -> T, T
---------
S
which seems an unsound reasoning principle as it would turn ex falso
quodlibet into negation.
Not beeing applicable in general, i'd like to explore the usefulness of
narrowing for computing with functions with domain Type during type
checking where the output of such functions is constrained to be a most
general type scheme.
I would not have dared to gate-crash with such vagueness if i had not
recently realized authoritative thought beeing spent on using narrowing
during type checking:
http://www.cl.cam.ac.uk/Research/LS/Talks/2005_06/2006-04-28.Sheard.html
Unfortunately there's no supplement available, so right now i'm scanning
the Omega docs for relevance.
Best regards,
Sebastian
