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 presevertation (Section 5).
We work through a simple program that closes terms with free variables using lambda abstractions. The example demonstrates pattern matching with contexts and using the built-in variable substitution.
Since Beluga does not support equality types, we implement equality using a LF type family eq as dependent kinds.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.