This guide is mostly for users who have only a background in functional programming as often taught in an undergraduate class. We show how to write some common simple functional programs in Beluga and also briefly discuss how to write simple proofs in Beluga.Here are a few sample programs discussed in the tutorial to get you started
- nat.bel: naturals (Section 2);
- yn.bel yes and no (Section 2);
- listnat.bel: Lists of naturals (Section 2);
- dtlist.bel: length indexed lists (Section 3);
- typesterms2.bel: list filtering (Section 3);
- typesterms3.bel: list filtering (Section 3);
- typesterms.bel: evaluation is deterministic (Section 4);
- lambda.bel: lambda-calculus and proof of preservation (Section 5).
We build a simple program that closes open terms, converting each free variable to one bound by a lambda abstraction. The example demonstrates pattern matching on contexts and Beluga's built-in mechanism for variable substitution.
The order of assumptions in a context is important in Beluga. However, sometimes the need to reorder assumptions arises, as is illustrated in the proof of the substitution lemma for algorithmic equality. As in Twelf this kind of proof does not come for free in Beluga.
In order to prove algorithmic equality for a polymorphic lambda-calculus, we establish schemas with alternating assumptions, depending on the type of the variable.
Since Beluga does not support equality types, we implement equality using an LF type family as a dependent kind. The difficulties of defining equality via reflexivity in Twelf do not arise in Beluga. Beluga's proof is implemented as a function using pattern matching instead of relations; as we pattern match we learn more about the given derivations and information flows as expected.
Context relationships can be defined explicitly using inductive datatypes. In this proof we use inductive datatypes to establish strengthening and weakening between contexts.
This example demonstrates Beluga's capacity for automatic context subsumption. If schema W is a prefix of a schema W0, then we can always use a context of schema W0 in place of a context of schema W. Essentially, we allow the user to pass a context of schema W0 where a context with schema W if W0 contains at least as much information as W.