blog/posts/beluga.md

80 lines
2.3 KiB
Markdown
Raw Normal View History

2022-09-17 14:56:50 -04:00
---
date: 2022-07-12
title: a few undocumented beluga features
tags: [computer, beluga, cool languages]
toc: true
2024-09-15 11:50:32 -04:00
summary: |
some undocumented features i found while looking through the source code
of the proof language beluga.
2022-09-17 14:56:50 -04:00
...
several of these are in the [examples], just not in the documentation. but some
of them i did find while looking through the parser.
[examples]: https://github.com/Beluga-lang/Beluga/tree/master/examples
## unicode
you can call your context variables `Γ` and it works just fine.
you can also use `→` and `⇒` and `⊢` if they are legible in the font you're
using.
## block values in substitutions
a lot of the time you have a variable typed like
`\[Γ, b : block (x : term, t : oft x A[..]) ⊢ ty]`,
but you actually need a
`\[Γ, x : term, t : oft x A[..] ⊢ ty]`,
with the block flattened out. or vice versa.
or you want to substitute the block more conveniently.
for this purpose, there is actually a block literal syntax `<a; b; c>` usable
in substitutions:
```beluga
let [Γ, b : block (x : term, t : oft x A[..]) ⊢ X] = blah in
[Γ, x : term, t : oft x A[..] ⊢ X[.., <x; t>]]
% but equivalent to this, but clearer (imo)
let [Γ, block (x : term, t : oft x A[..]) ⊢ X[.., b.x, b.t]] = blah in
[Γ, x : term, t : oft x A[..] ⊢ X]
```
## explicit binders before patterns
sometimes in a case expression, the type of the pattern variables is too hard
for beluga to work out on its own. in this case you get an error message about
a stuck unification problem.
most of the time you can get out of this by writing the types of some variables
explicitly. the syntax is like a forall-type:
```beluga
case [Γ ⊢ #p] of
| {#p : [Γ ⊢ term]}
[Γ, y : term ⊢ #p[..]] ⇒ ?body
```
## mutual recursion
of course this exists. but it's not mentioned anywhere in the documentation for
some reason. the syntax is this:
```beluga
LF term : type = …
and elim : type = …;
rec eval-term : (Γ : ctx) [Γ ⊢ term] → [Γ ⊢ value] = …
and rec eval-elim : (Γ : ctx) [Γ ⊢ elim] → [Γ ⊢ value] = …;
inductive ReduceTerm : (Γ : ctx) [Γ ⊢ term] → ctype = …
and inductive ReduceElim : (Γ : ctx) [Γ ⊢ elim] → ctype = …;
```
two `rec`s! which is because you can mix `rec`/`proof`, or
`inductive`/`coinductive`/`stratified`, within a block.