77 lines
2.2 KiB
Markdown
77 lines
2.2 KiB
Markdown
|
---
|
||
|
|
date: 2022-07-12
|
||
|
|
title: a few undocumented beluga features
|
||
|
|
tags: [computer, beluga, cool languages]
|
||
|
|
toc: true
|
||
|
|
...
|
||
|
|
|
||
|
|
|
||
|
|
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.
|