[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
The Delphin Programming Language: Functional programming over LF
-------------------------
Delphin is a functional programming language that utilizes LF for its
datatypes. The key difficulties that we address are in supporting
computation over higher-order encodings as well as supporting dependent
types. When programming in languages like ML, Haskell, or even Twelf, the
notion of "context" and "substitution" are meta-level concepts hidden to
the programmer and they remain hidden in our system.
We support computation over higher-order encodings by distinguishing
between two methods of variable binding. A function can be written as fn
x => e. This has the standard meaning of a function, where the binding
x is intended for instantiation. The computation of e is triggered by
application which first instantiates the x.
Alternatively, we provide a newness constructor binding variables that
will always remain uninstantiated. We write "{<x>}e", and the evaluation
of e occurs while the binding x is uninstantiated. Therefore, for the
scope of e, the variable x behaves as a fresh constant, which we call a
"parameter". Delphin pervasively distinguishes between parameters and
objects and typing statically guarantees that parameters cannot escape
their scope.
A submitted paper describing the underlying calculus of Delphin is at:
http://cs-www.cs.yale.edu/homes/delphin/files/popl08-submission.pdf
You are invited to try out our implementation available at:
http://cs-www.cs.yale.edu/homes/delphin/delphin.htm
(You will need SML/NJ or PolyML to install it)
We welcome your feedback as well as any questions. There are many
examples illustrating Delphin on the website. These examples range from
simple addition, to combinator transformations, to an example of type
inference using parameters instead of the typical references.
Please direct your comments/questions to [EMAIL PROTECTED] .
Thank you.
Adam Poswolsky
[EMAIL PROTECTED]
