posts
This commit is contained in:
parent
3f827564b4
commit
9f850de9ba
14 changed files with 325 additions and 375 deletions
189
chrismas.md
189
chrismas.md
|
|
@ -1,189 +0,0 @@
|
||||||
<!DOCTYPE html>
|
|
||||||
<html>
|
|
||||||
<meta charset=utf-8>
|
|
||||||
|
|
||||||
<link rel=stylesheet href=/style/page.css>
|
|
||||||
|
|
||||||
|
|
||||||
<title></title>
|
|
||||||
|
|
||||||
|
|
||||||
<header>
|
|
||||||
<h1>merr chrismas</h1>
|
|
||||||
<div class=meta>
|
|
||||||
<h2 class=date>monday 25 december 2023</h2>
|
|
||||||
<nav class=tags>
|
|
||||||
tags:
|
|
||||||
<ul>
|
|
||||||
<li><a href=/tag-l_ntas.html>lántas</a>
|
|
||||||
<li><a href=/tag-conlangs.html>conlangs</a>
|
|
||||||
</ul>
|
|
||||||
</nav>
|
|
||||||
</div>
|
|
||||||
<hr>
|
|
||||||
</header>
|
|
||||||
|
|
||||||
|
|
||||||
<main>
|
|
||||||
# just tell me how to say it please
|
|
||||||
|
|
||||||
sure thing. here.
|
|
||||||
|
|
||||||
```{=html}
|
|
||||||
<figure class="glosses">
|
|
||||||
```
|
|
||||||
---------------------------------------------------------------------- ----------------------------------------------------
|
|
||||||
{.scr .laantas}
|
|
||||||
ufit þulkussarim
|
|
||||||
\[ˌufit ˈθuɫkɔsːɐʑɪ̃\]
|
|
||||||
ufi--t þulkus(i)--sa--ri--m
|
|
||||||
cozy--[GEN]{.abbr} midwinter--[AD]{.abbr}--[PRL]{.abbr}--[DEF]{.abbr}
|
|
||||||
(be) cozy during midwinter
|
|
||||||
---------------------------------------------------------------------- ----------------------------------------------------
|
|
||||||
|
|
||||||
```{=html}
|
|
||||||
</figure>
|
|
||||||
```
|
|
||||||
# details
|
|
||||||
|
|
||||||
now i am not a huge fan of putting christianity into my conlang, which
|
|
||||||
is hopefully understandable. but having a midwinter festival sounds
|
|
||||||
cute. the days are finally getting longer! you made it through the worst
|
|
||||||
part! and so on. so that's what this is. i think it probably takes place
|
|
||||||
the day after the solstice, but with several days of festivities, so
|
|
||||||
that there is still a little overlap with the *other* winter holiday.
|
|
||||||
it's still appropriate to say it today.
|
|
||||||
|
|
||||||
## seasons
|
|
||||||
|
|
||||||
time name pron. translation
|
|
||||||
---------- --------------------------------------------------------------- ------------------- ---------------------------------- -------------
|
|
||||||
nov--jan [{.scr .laantas}]{.lang} [igisim]{.lang} [\[ˈiʝɛsĩ\]]{.ipa .ipa-narrow} the freeze
|
|
||||||
feb [{.scr .laantas}]{.lang} [susurum]{.lang} [\[ˈsusʊrõ\]]{.ipa .ipa-narrow} the melt
|
|
||||||
mar--may [{.scr .laantas}]{.lang} [šangubam]{.lang} [\[ˈʃaŋɡɔvɑ̃\]]{.ipa .ipa-narrow} the bloom
|
|
||||||
jun--aug [{.scr .laantas}]{.lang} [guwanḿ]{.lang} [\[ˈɡɔwɑnm̩\]]{.ipa .ipa-narrow} the sun
|
|
||||||
sep--oct [{.scr .laantas}]{.lang} [santum]{.lang} [\[ˈsantõ\]]{.ipa .ipa-narrow} the rain
|
|
||||||
|
|
||||||
- in between [{.scr
|
|
||||||
.laantas}[igisim]{.text}]{.lang} (winter) and
|
|
||||||
[{.scr
|
|
||||||
.laantas}[šangubam]{.text}]{.lang} (spring), the month of february
|
|
||||||
is considered a transition between the two,
|
|
||||||
[{.scr
|
|
||||||
.laantas}[susurum]{.text}]{.lang}.
|
|
||||||
- as a result, [{.scr
|
|
||||||
.laantas}[santum]{.text}]{.lang} (autumn) is only two months long.
|
|
||||||
- [{.scr
|
|
||||||
.laantas}[šangubam]{.text}]{.lang} comes from
|
|
||||||
[{.scr .laantas}[šani]{.text}]{.lang}
|
|
||||||
(flower) and [{.scr
|
|
||||||
.laantas}[guba]{.text}]{.lang} (grow, thrive).
|
|
||||||
|
|
||||||
## putting it together
|
|
||||||
|
|
||||||
the word "midwinter", without any inflections, is
|
|
||||||
[{.scr
|
|
||||||
.laantas}[þulkusim]{.text}]{.lang}, which comes from
|
|
||||||
[{.scr .laantas}[þulku]{.text}]{.lang}
|
|
||||||
"be deep" and [{.scr
|
|
||||||
.laantas}[igisim]{.text}]{.lang}. unusually for lántas,
|
|
||||||
[{.scr .laantas}[þulku]{.text}]{.lang} is
|
|
||||||
a verb, rather than a noun. why? who knows.
|
|
||||||
|
|
||||||
```{=html}
|
|
||||||
<aside class='floating'>
|
|
||||||
```
|
|
||||||
on that page, where you see a [ƶ]{.lang}, replace it with [þ]{.lang}. i
|
|
||||||
haven't got round to updating that yet. it also has the ugly text until
|
|
||||||
i redraw [{.scr
|
|
||||||
.laantas}[č ǧ]{.text}]{.lang}, since at least if it's all ugly it's
|
|
||||||
consistent. sorry about that.
|
|
||||||
|
|
||||||
```{=html}
|
|
||||||
</aside>
|
|
||||||
```
|
|
||||||
the suffix [{.scr
|
|
||||||
.laantas}[--sari]{.text}]{.lang} is actually a pair of two suffixes,
|
|
||||||
which together mean through, or during. the details of the whole
|
|
||||||
situation are
|
|
||||||
[here](https://lang.niss.website/laantas/nouns.html#locational-cases),
|
|
||||||
but it is a cool two-dimensional system based on a thing that can be
|
|
||||||
found in some languages of the caucasus. the
|
|
||||||
[{.scr .laantas}[--m]{.text}]{.lang} on the end
|
|
||||||
(of all these words so far, actually) is "the". so the full form
|
|
||||||
[{.scr
|
|
||||||
.laantas}[þulkusisarim]{.text}]{.lang} means "during midwinter", and
|
|
||||||
that one [i]{.lang} is dropped in this phrase to give the form
|
|
||||||
[{.scr
|
|
||||||
.laantas}[þulkussarim]{.text}]{.lang}.
|
|
||||||
|
|
||||||
now, for [{.scr
|
|
||||||
.laantas}[ufit]{.text}]{.lang}. there is a small, but technically
|
|
||||||
non-zero, chance that you remember the word
|
|
||||||
[{.scr
|
|
||||||
.laantas}[uf`<u>`{=html}a`</u>`{=html}t]{.text}]{.lang} from
|
|
||||||
[here](https://cohost.org/niss/post/3366713-ufat-iksaha), with the
|
|
||||||
meaning of "warm". this is actually the same word, but a bit cutesy. it
|
|
||||||
means cozy.
|
|
||||||
|
|
||||||
the implied verb in this sentence is
|
|
||||||
[{.scr
|
|
||||||
.laantas}[iksaha]{.text}]{.lang}, like before. this is an auxiliary verb
|
|
||||||
for requests. for example, if [{.scr
|
|
||||||
.laantas}[šikkúha]{.text}]{.lang} means "you are going", then
|
|
||||||
[{.scr
|
|
||||||
.laantas}[šikkúm iksaha]{.text}]{.lang} means "please go away". the
|
|
||||||
[--ha]{.lang} here means "you" (singular). here it's dropped because the
|
|
||||||
phrase is long enough already to be easily understood.
|
|
||||||
|
|
||||||
so in the end, you get
|
|
||||||
[{.scr
|
|
||||||
.laantas}[ufit þulkussarim]{.text}]{.lang}, meaning "\[stay\] cozy
|
|
||||||
during the midwinter".
|
|
||||||
|
|
||||||
::: twocol-grid
|
|
||||||
{width="100%"}
|
|
||||||
|
|
||||||
```{=html}
|
|
||||||
<figure class="glosses left">
|
|
||||||
```
|
|
||||||
---------------------------------------------------------- ----
|
|
||||||
{.scr .laantas}
|
|
||||||
þugusim ai
|
|
||||||
\[ˈθuɣɔsĩm‿ai\]
|
|
||||||
þugusi--m ai
|
|
||||||
miwiner--[DEF]{.abbr} be
|
|
||||||
it crismas
|
|
||||||
---------------------------------------------------------- ----
|
|
||||||
|
|
||||||
```{=html}
|
|
||||||
</figure>
|
|
||||||
```
|
|
||||||
{width="100%"}
|
|
||||||
|
|
||||||
```{=html}
|
|
||||||
<figure class="glosses left">
|
|
||||||
```
|
|
||||||
------------------------------------------------------------------ ----------------------------------------
|
|
||||||
{.scr .laantas}
|
|
||||||
ufi þugussarim
|
|
||||||
\[ˌufi ˈθuɣɔsːɐʑĩ\]
|
|
||||||
ufi--(t) þugus(i)--sari--m
|
|
||||||
cozy--([GEN]{.abbr}) miwiner--[DURING]{.abbr}--[DEF]{.abbr}
|
|
||||||
merr crismas
|
|
||||||
------------------------------------------------------------------ ----------------------------------------
|
|
||||||
|
|
||||||
```{=html}
|
|
||||||
</figure>
|
|
||||||
```
|
|
||||||
:::
|
|
||||||
|
|
||||||
</main>
|
|
||||||
|
|
||||||
|
|
||||||
<footer>
|
|
||||||
<hr>
|
|
||||||
<a href=/index.html>all posts</a> ·
|
|
||||||
<a href=/all-tags.html>all tags</a>
|
|
||||||
</footer>
|
|
||||||
|
|
||||||
BIN
images/quorientation.png
Normal file
BIN
images/quorientation.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 509 KiB |
BIN
images/skip-some-floors.png
Normal file
BIN
images/skip-some-floors.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 10 KiB |
|
|
@ -1,177 +0,0 @@
|
||||||
---
|
|
||||||
title: quox. the language
|
|
||||||
date: 2023-10-25
|
|
||||||
tags: [quox, computer, types]
|
|
||||||
bibliography: quox.bib
|
|
||||||
link-citations: true
|
|
||||||
show-toc: true
|
|
||||||
...
|
|
||||||
|
|
||||||
<style>
|
|
||||||
header h1 { margin-left: 0; }
|
|
||||||
header h1::before, header h1::after {
|
|
||||||
content: url(../images/qt.svg);
|
|
||||||
display: inline-block;
|
|
||||||
height: 0.75em; width: 0.75em;
|
|
||||||
padding: 0 0.5em;
|
|
||||||
}
|
|
||||||
header h1::before {
|
|
||||||
transform: rotateY(0.5turn);
|
|
||||||
}
|
|
||||||
main > :is(h1, h2, h3, h4, h5, h6)::after {
|
|
||||||
content: url(../images/quox-tod.png);
|
|
||||||
image-rendering: crisp-edges;
|
|
||||||
image-rendering: pixelated;
|
|
||||||
margin-left: 0.5em;
|
|
||||||
}
|
|
||||||
.qtt-q { font-family: Muller; font-weight: 600; color: #60c; }
|
|
||||||
.xtt-x { font-family: Muller; font-weight: 600; color: #082; }
|
|
||||||
|
|
||||||
#panqt {
|
|
||||||
--width: 202px; --height: 200px;
|
|
||||||
}
|
|
||||||
#panqt div {
|
|
||||||
width: var(--width); height: var(--height);
|
|
||||||
position: relative;
|
|
||||||
}
|
|
||||||
#panqt img, #panqt div::before {
|
|
||||||
position: absolute;
|
|
||||||
top: 0; left: 0;
|
|
||||||
width: var(--width); height: var(--height);
|
|
||||||
}
|
|
||||||
#panqt div::before {
|
|
||||||
content:
|
|
||||||
image-set(url(../images/panqt.png) 1x,
|
|
||||||
url(../images/panqt2x.png) 2x);
|
|
||||||
mix-blend-mode: multiply;
|
|
||||||
}
|
|
||||||
#panqt figcaption {
|
|
||||||
width: var(--width);
|
|
||||||
}
|
|
||||||
</style>
|
|
||||||
|
|
||||||
|
|
||||||
:::{.aside .floating}
|
|
||||||
### [hot minute](https://en.wiktionary.org/wiki/hot_minute) <i>n.</i> {.unnumbered}
|
|
||||||
|
|
||||||
1. A long period of time.
|
|
||||||
2. A short period of time.
|
|
||||||
3. An unspecified period of time.
|
|
||||||
:::
|
|
||||||
|
|
||||||
for the last _hot minute_ [@hotminute], i’ve been working on a little programming language. it’s finally starting to approach a state where it can compile some programs, so maybe i should talk about it a bit.
|
|
||||||
|
|
||||||
|
|
||||||
# what is a quox [(tl;dr for type system nerds)]{.note}
|
|
||||||
|
|
||||||
<figure class=floating>
|
|
||||||
<img src=../images/quox.png class='shadow pixel'
|
|
||||||
alt='a dragon from an old arcade game'
|
|
||||||
title='use my warps to skip some floors!'>
|
|
||||||
<figcaption>this is also a quox.</figcaption>
|
|
||||||
</figure>
|
|
||||||
|
|
||||||
0. it’s a *dependently typed functional language*, like your agdas and your idrises.
|
|
||||||
1. it has a *closed type universe*. you don’t define new datatypes, but the language gives you building blocks to put them together.
|
|
||||||
2. *[q]{.qtt-q}uantitative type theory* (qtt) [@nuttin; @qtt] is a nice combination of dependent types, resource tracking, and erasure of stuff like proofs.
|
|
||||||
3. *[x]{.xtt-x}tt* [@xtt], which `*i sure hope i remember to come back and add this!*`
|
|
||||||
- the closed type universe is a consequence of xtt (as well as its kinda-predecessor ott [@ott-now]), but i decided to just run with it.
|
|
||||||
- “xtt” stands for “extensional type theory”, but it’s not _that_ extensional type theory. i know. not my fault.
|
|
||||||
|
|
||||||
so now you can see where the name [q]{.qtt-q}uo[x]{.xtt-x} comes from. other than my favourite dragon. anyway it also has
|
|
||||||
|
|
||||||
<figure class=floating id=panqt>
|
|
||||||
<div><img src=../images/panqt.nobg.png srcset='../images/panqt.nobg2x.png 2x'
|
|
||||||
width=202 height=200
|
|
||||||
alt='one of my fursonas is a quox with three heads'
|
|
||||||
title='i hear putting pictures of your fursona on your blog is a good way to get hacker news types Big Mad if they find out about it'></div>
|
|
||||||
<figcaption>
|
|
||||||
sometimes i am also a quox. or three, depending on how you count.
|
|
||||||
</figcaption>
|
|
||||||
</figure>
|
|
||||||
|
|
||||||
4. *bidirectional type checking* [@bidi] `*this one too*`
|
|
||||||
5. crude-but-effective stratification [@crude; @crude-blog] for dealing with universes. `*does this need more detail too?*`
|
|
||||||
6. *written in idris2*. that doesn’t really have much impact on the language itself, other than the compilation process, but i’m enjoying using a dependently typed language for something substantial. even if it’s one you’re not currently supposed to be using for anything substantial. also currently it spits out scheme, like idris, because that was easy.
|
|
||||||
7. all the non-ascii syntax is [optional], but i like it.
|
|
||||||
|
|
||||||
[optional]: https://git.rhiannon.website/rhi/quox/wiki/ascii-syntax
|
|
||||||
|
|
||||||
as for what it _doesn’t_ have: any but the most basic of conveniences. sorry.
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
# dependent types
|
|
||||||
|
|
||||||
there are lots of languages with dependent types—well, quite a few—so i won’t spend too much time on this.
|
|
||||||
|
|
||||||
`*but still something*`
|
|
||||||
|
|
||||||
|
|
||||||
# closed type universe
|
|
||||||
|
|
||||||
instead of having datatypes like in normal languages, in quox you get the basic building blocks to make them. the main building blocks are functions, pairs, enumerations, equality types, strings, and natural numbers. some sort of syntactic sugar to expand a datatype declaration into this representation _is_ something i want to add, but it'd be in the pretty distant future.
|
|
||||||
|
|
||||||
:::aside
|
|
||||||
_at the moment_, natural numbers are the only recursion possible. so you can define types with the same recursive structure, like lists, but binary trees and stuff are not _currently_ possible, until i replace them with something more general. probably w-types [@nlab-wtype].
|
|
||||||
:::
|
|
||||||
|
|
||||||
but right now you can define a few types like this. see [qtt](#qtt) below for what all the `0`s and `ω`s mean. due to the lack of generic recursion, but the presence of _natural numbers_ specifically, a list is a length, followed by a nested tuple of that length (terminated by `'nil`).
|
|
||||||
|
|
||||||
```quox
|
|
||||||
def0 Vec : ℕ → ★ → ★ =
|
|
||||||
λ n A ⇒
|
|
||||||
case n return ★ of {
|
|
||||||
zero ⇒ {nil};
|
|
||||||
succ p, As ⇒ A × As
|
|
||||||
} -- ↖ As = Vec p A
|
|
||||||
|
|
||||||
def0 List : ★ → ★ = λ A ⇒ (n : ℕ) × Vec n A
|
|
||||||
|
|
||||||
def Nil : 0.(A : ★) → List A = λ A ⇒ (0, 'nil)
|
|
||||||
def Cons : 0.(A : ★) → A → List A → List A =
|
|
||||||
λ A x xs ⇒ case xs return List A of { (len, xs) ⇒ (succ len, x, xs) }
|
|
||||||
|
|
||||||
def NilS = Nil String
|
|
||||||
def ConsS = Cons String
|
|
||||||
|
|
||||||
def example = ConsS "im" (ConsS "gay" NilS)
|
|
||||||
|
|
||||||
def0 example-eq : example ≡ (2, "im", "gay", 'nil) : List String =
|
|
||||||
refl (List String) example
|
|
||||||
```
|
|
||||||
|
|
||||||
you might have noticed that i didn't write the eliminator. that is because they are kind of ugly. if you want to see it anyway you can find it in [the example folder][ex].
|
|
||||||
|
|
||||||
[ex]: https://git.rhiannon.website/rhi/quox/src/commit/246d80eea2/examples/list.quox#L12-L25
|
|
||||||
|
|
||||||
|
|
||||||
# qtt
|
|
||||||
|
|
||||||
sometimes, values of some type can only be used in certain ways to make sense. this is hardly controversial; if you do this with
|
|
||||||
|
|
||||||
|
|
||||||
a problem that dependent types used to have a lot is that the blurring of compile-time and run-time data can lead to more being retained than necessary.
|
|
||||||
|
|
||||||
`*is there an example that has superlinear junk data without resorting to peano naturals or some shit*`
|
|
||||||
|
|
||||||
consider this vector (length-indexed list) definition from a _hypothetical language_ with normal inductive types.
|
|
||||||
|
|
||||||
```agda
|
|
||||||
data Vect (A : ★) : ℕ → ★ where
|
|
||||||
[] : Vect A 0
|
|
||||||
_∷_ : (n : ℕ) → A → Vect A n → Vect A (succ n)
|
|
||||||
```
|
|
||||||
|
|
||||||
in a totally naive implementation, `cons` would store `n`, the length of its tail (and maybe even some kind of representation of `A` too). so a three element list would look something like
|
|
||||||
|
|
||||||
|
|
||||||
# xtt
|
|
||||||
|
|
||||||
`*mention about type-case and the closed universe*`
|
|
||||||
|
|
||||||
|
|
||||||
# bidirectional type checking
|
|
||||||
|
|
||||||
|
|
||||||
# references {#refs}
|
|
||||||
67
posts-wip/qpoly.md
Normal file
67
posts-wip/qpoly.md
Normal file
|
|
@ -0,0 +1,67 @@
|
||||||
|
---
|
||||||
|
title: quantity polymorphism (draft)
|
||||||
|
date: 2024-04-21
|
||||||
|
tags: [quox, computer]
|
||||||
|
...
|
||||||
|
|
||||||
|
|
||||||
|
im getting sick of writing `elim` and `elimω`, and `fold` and `foldω` and—
|
||||||
|
|
||||||
|
so let's call the quantity context, uh, $Ξ$. it's just a list of bound vars.
|
||||||
|
quantity arguments have to be full expressions though because arithmetic shows
|
||||||
|
up in the typing rules
|
||||||
|
|
||||||
|
## syntax
|
||||||
|
|
||||||
|
:::texdefs
|
||||||
|
$$ \newcommand\HL{\textcolor{blueviolet}} $$
|
||||||
|
:::
|
||||||
|
|
||||||
|
|
||||||
|
$$
|
||||||
|
\begin{aligned}
|
||||||
|
D &::=
|
||||||
|
\cdots \mid \mathtt{def} \; \mathsf{a}_{\HL{\overline α}} : A = s
|
||||||
|
& \text{declarations} \\
|
||||||
|
e &::=
|
||||||
|
\cdots \mid \mathsf{a}_{\HL{\overline π}}^{ℓ}
|
||||||
|
& \text{eliminations} \\
|
||||||
|
π, ρ &::=
|
||||||
|
𝔮 \HL{\mid α \mid π + ρ \mid π \cdot ρ}
|
||||||
|
& \HL{\text{quantity expressions}} \\[1em]
|
||||||
|
\HL{α, β} && \HL{\text{quantity variables}} \\
|
||||||
|
𝔮 &::=
|
||||||
|
0 \mid 1 \mid ω
|
||||||
|
& \text{quantity constants} \\
|
||||||
|
\HL{Ξ} &\mathrel{\HL{::=}}
|
||||||
|
\HL{\cdot \mid Ξ, α}
|
||||||
|
& \HL{\text{quantity contexts}}
|
||||||
|
\end{aligned}
|
||||||
|
$$
|
||||||
|
|
||||||
|
- a _quantity value_ $π̃$ in a context $Ξ$ is a polynomial with variables from
|
||||||
|
$Ξ$ and coefficients from $\{0,1,ω\}$.
|
||||||
|
|
||||||
|
|
||||||
|
## typing
|
||||||
|
|
||||||
|
:::texdefs
|
||||||
|
$$
|
||||||
|
\newcommand\FracS[2]{\frac{\;#1\;}{\;#2\;}}
|
||||||
|
\newcommand\Many[1]{\begin{gathered}#1\end{gathered}}
|
||||||
|
\newcommand\Rule[3][]{\FracS{\Many{#2}}{\Many{#3}}\;\text{\small[#1]}}
|
||||||
|
\newenvironment{Rules}
|
||||||
|
{\begin{gathered}\newcommand\nl{\\[1em]}}
|
||||||
|
{\end{gathered}}
|
||||||
|
$$
|
||||||
|
:::
|
||||||
|
|
||||||
|
:::rulebox
|
||||||
|
$$
|
||||||
|
\newcommand\Syn\Rightarrow \newcommand\Chk\Leftarrow
|
||||||
|
\begin{gathered}
|
||||||
|
\HL{Ξ \mid} Ψ \mid Γ \vdash σ \cdot s \Chk A \rhd Σ \\
|
||||||
|
\HL{Ξ \mid} Ψ \mid Γ \vdash σ \cdot e \Syn A \rhd Σ
|
||||||
|
\end{gathered}
|
||||||
|
$$
|
||||||
|
:::
|
||||||
95
posts-wip/record.md
Normal file
95
posts-wip/record.md
Normal file
|
|
@ -0,0 +1,95 @@
|
||||||
|
---
|
||||||
|
title: records
|
||||||
|
date: 2024-06-02
|
||||||
|
tags: ['quox (language)']
|
||||||
|
...
|
||||||
|
|
||||||
|
n-ary products to replace pairs _and_ boxes, since the nested `case`
|
||||||
|
expressions for nested pairs are actually really annoying.
|
||||||
|
|
||||||
|
# syntax
|
||||||
|
|
||||||
|
$$
|
||||||
|
\newcommand\CEQ{\operatorname{::=}}
|
||||||
|
\begin{aligned}
|
||||||
|
A, B, s, t &\CEQ \dotsb
|
||||||
|
\mid ꞌ[Δ]
|
||||||
|
\mid [𝔇]
|
||||||
|
& \text{terms} \\
|
||||||
|
e, f &\operatorname{::=} \dotsb
|
||||||
|
\mid e\mathord·ℓ
|
||||||
|
& \text{eliminations} \\
|
||||||
|
𝔅 &\operatorname{::=} \dotsb
|
||||||
|
\mid [ \overline{ℓ=x} ] ⇒ s
|
||||||
|
& \text{case bodies} \\[1em]
|
||||||
|
ℓ &\operatorname{::=} x \mid n & \text{labels ($n ∈ ℕ$)} \\[1em]
|
||||||
|
Δ &\operatorname{::=} \overline{π· ℓ=x : A} & \text{telescopes} \\
|
||||||
|
𝔇 &\operatorname{::=} \overline{ℓ=s} & \text{list of bindings} \\
|
||||||
|
ϕ &\operatorname{::=} \overline{x=e} & \text{substitutions} \\
|
||||||
|
\end{aligned}
|
||||||
|
$$
|
||||||
|
|
||||||
|
- this __replaces__ the box syntax. pair syntax __still exists__ but
|
||||||
|
expands to this. this means that
|
||||||
|
$A \times B \times C$ and $A \times (B \times C)$ are no longer equivalent.
|
||||||
|
i guess that's fine but it is a change.
|
||||||
|
- overlined things are comma separated.
|
||||||
|
- in $Δ$, $π$ is optional and defaults to $1$ like everywhere else.
|
||||||
|
- the pair syntax
|
||||||
|
$(x_0, \dotsc, x_n) : (x_0 : A_0) \times \dotsb \times A_n$
|
||||||
|
is now an abbreviation for
|
||||||
|
$ꞌ[0=x_0, \dotsc, n=x_n] : [0=x_0: A_0, \dotsc, n: A_n]$.
|
||||||
|
- instead of $\operatorname{\mathsf{fst}} e$ and $\operatorname{\mathsf{snd}} e$, it's now $e\mathord.0$
|
||||||
|
and $e\mathord.1$ (and $e\mathord.2$, …).
|
||||||
|
- "`'[0. 0 : A]`" looks bad. i know.
|
||||||
|
- a telescope $Δ$ can be used as a context by ignoring the outer labels $ℓ$.
|
||||||
|
|
||||||
|
# typing
|
||||||
|
|
||||||
|
## telescope checking
|
||||||
|
|
||||||
|
:::rulebox
|
||||||
|
$$Γ ⊢ Δ$$
|
||||||
|
:::
|
||||||
|
|
||||||
|
$$
|
||||||
|
\frac{}{Γ ⊢ •}
|
||||||
|
\qquad
|
||||||
|
\frac{
|
||||||
|
Γ ⊢ Δ \qquad
|
||||||
|
Γ, Δ ⊢_0 A ⇐ ★
|
||||||
|
}{
|
||||||
|
Γ ⊢ Δ, π·ℓ = x : A
|
||||||
|
}
|
||||||
|
$$
|
||||||
|
|
||||||
|
## binding list checking
|
||||||
|
|
||||||
|
:::rulebox
|
||||||
|
$$ Γ ⊢ σ·𝔇 ⇐ Δ ⊳ Σ $$
|
||||||
|
:::
|
||||||
|
|
||||||
|
$$ \frac{}{Γ ⊢ σ·• ⇐ • ⊳ 𝟎} $$
|
||||||
|
|
||||||
|
$$
|
||||||
|
\frac{
|
||||||
|
Γ ⊢ σ·𝔇 ⇐ Δ ⊳ Σ_𝔇 \qquad
|
||||||
|
Γ ⊢ ⌊σπ⌋ · s ⇐ A[𝔇:Δ] ⊳ Σ_s
|
||||||
|
}{
|
||||||
|
Γ ⊢ σ· (𝔇, ℓ = s) ⇐ (Δ, π·ℓ = x : A) ⊳ Σ_𝔇 + πΣ_s
|
||||||
|
}
|
||||||
|
$$
|
||||||
|
|
||||||
|
:::rulebox
|
||||||
|
$$ 𝔇 : Δ = ϕ $$
|
||||||
|
:::
|
||||||
|
|
||||||
|
produce a substitution from a binding list and a telescope by distributing the
|
||||||
|
type annotations
|
||||||
|
|
||||||
|
$$
|
||||||
|
\begin{aligned}
|
||||||
|
• : • &= • \\
|
||||||
|
(𝔇, x = s) : (Δ, π·ℓ=x : A) &= (𝔇 : Δ), (x = s ∷ A)
|
||||||
|
\end{aligned}
|
||||||
|
$$
|
||||||
12
posts/ats.md
12
posts/ats.md
|
|
@ -3,6 +3,8 @@ title: a little ats program
|
||||||
date: 2022-09-16
|
date: 2022-09-16
|
||||||
tags: [computer, ATS, cool languages]
|
tags: [computer, ATS, cool languages]
|
||||||
show-toc: true
|
show-toc: true
|
||||||
|
summary: |
|
||||||
|
a little program in a little-known, little-documented language called ATS.
|
||||||
...
|
...
|
||||||
|
|
||||||
[ats] is a language that is a little infamous among type system likers, for its
|
[ats] is a language that is a little infamous among type system likers, for its
|
||||||
|
|
@ -60,9 +62,7 @@ let's start by defining the syntax for types. it's going to be a single base
|
||||||
type, and functions.
|
type, and functions.
|
||||||
|
|
||||||
$$
|
$$
|
||||||
\newcommand\Typ{\mathit{typ}}
|
A, B \operatorname{::=} \mathord• \mid A → B
|
||||||
\newcommand\OR{\mathrel|}
|
|
||||||
\Typ ::= \bullet \OR \Typ_1 \to \Typ_2
|
|
||||||
$$
|
$$
|
||||||
|
|
||||||
so obviously, my first attempt was to just write this:
|
so obviously, my first attempt was to just write this:
|
||||||
|
|
@ -159,11 +159,7 @@ overload print with print_typ
|
||||||
types are done, now let's move on to terms. we just want names, lambdas, and
|
types are done, now let's move on to terms. we just want names, lambdas, and
|
||||||
application.
|
application.
|
||||||
|
|
||||||
$$
|
$$ s, t \operatorname{::=} x \mid λ x : A. s \mid s \; t $$
|
||||||
\newcommand\Term{\mathit{term}}
|
|
||||||
\newcommand\Var{\mathit{var}}
|
|
||||||
\Term ::= \Var \OR \lambda \Var : \Typ. \Term \OR \Term_1 \; \Term_2
|
|
||||||
$$
|
|
||||||
|
|
||||||
for the same reason as before, terms are indexed by their height, but _also_ by
|
for the same reason as before, terms are indexed by their height, but _also_ by
|
||||||
the number of variables in scope, since i want de bruijn indices to be
|
the number of variables in scope, since i want de bruijn indices to be
|
||||||
|
|
|
||||||
|
|
@ -3,6 +3,9 @@ date: 2022-07-12
|
||||||
title: a few undocumented beluga features
|
title: a few undocumented beluga features
|
||||||
tags: [computer, beluga, cool languages]
|
tags: [computer, beluga, cool languages]
|
||||||
toc: true
|
toc: true
|
||||||
|
summary: |
|
||||||
|
some undocumented features i found while looking through the source code
|
||||||
|
of the proof language beluga.
|
||||||
...
|
...
|
||||||
|
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -3,6 +3,11 @@ date: 2023-12-25
|
||||||
title: merr chrismas
|
title: merr chrismas
|
||||||
tags: [lántas, conlangs]
|
tags: [lántas, conlangs]
|
||||||
conlang: laantas
|
conlang: laantas
|
||||||
|
summary: |
|
||||||
|
how to say "merr chrismas" in my conlang lántas.
|
||||||
|
|
||||||
|
if you don't care about the details, the answer is
|
||||||
|
“ufit þulkusimari”.
|
||||||
...
|
...
|
||||||
|
|
||||||
# just tell me how to say it please
|
# just tell me how to say it please
|
||||||
|
|
@ -74,7 +79,7 @@ so in the end, you get `{!ufit þulkusimsari}`, meaning "[stay] cozy during the
|
||||||
midwinter".
|
midwinter".
|
||||||
|
|
||||||
|
|
||||||
:::twocol-grid
|
::: {.twocol-grid .light}
|
||||||
{width=100%}
|
{width=100%}
|
||||||
|
|
||||||
::: {.glosses .left}
|
::: {.glosses .left}
|
||||||
|
|
|
||||||
|
|
@ -2,6 +2,9 @@
|
||||||
title: digitle in maude
|
title: digitle in maude
|
||||||
date: 2022-03-14
|
date: 2022-03-14
|
||||||
tags: [maude, computer, cool languages]
|
tags: [maude, computer, cool languages]
|
||||||
|
summary: |
|
||||||
|
a solver for digitle (numbers countdown) in maude, a language
|
||||||
|
for rewriting systems.
|
||||||
...
|
...
|
||||||
|
|
||||||
so you know [digitle] right. it's the countdown numbers round.
|
so you know [digitle] right. it's the countdown numbers round.
|
||||||
|
|
|
||||||
|
|
@ -2,6 +2,8 @@
|
||||||
title: fibonacci in maude and ats
|
title: fibonacci in maude and ats
|
||||||
date: 2022-10-24
|
date: 2022-10-24
|
||||||
tags: [computer, maude, ATS]
|
tags: [computer, maude, ATS]
|
||||||
|
summary: |
|
||||||
|
fibonacci numbers in the languages maude and ATS.
|
||||||
...
|
...
|
||||||
|
|
||||||
i might submit these [here], if i can be bothered to get a new github account.
|
i might submit these [here], if i can be bothered to get a new github account.
|
||||||
|
|
|
||||||
|
|
@ -2,6 +2,10 @@
|
||||||
title: undocumented idris2 features
|
title: undocumented idris2 features
|
||||||
date: 2022-11-12
|
date: 2022-11-12
|
||||||
tags: [computer, idris]
|
tags: [computer, idris]
|
||||||
|
summary: |
|
||||||
|
some lesser-known features in the dependently-typed language
|
||||||
|
idris (2).
|
||||||
|
|
||||||
header-includes: |
|
header-includes: |
|
||||||
<style>
|
<style>
|
||||||
.sidebyside {
|
.sidebyside {
|
||||||
|
|
|
||||||
141
posts/quorientation.md
Normal file
141
posts/quorientation.md
Normal file
|
|
@ -0,0 +1,141 @@
|
||||||
|
---
|
||||||
|
date: 2024-03-14
|
||||||
|
title: quorientation
|
||||||
|
tags: [lántas, conlangs]
|
||||||
|
conlang: laantas
|
||||||
|
summary: |
|
||||||
|
in my latest art, i put some text in my conlang lántas. here is approximately
|
||||||
|
too much detail about that.
|
||||||
|
...
|
||||||
|
|
||||||
|
<figure>
|
||||||
|
<a href=http://gallery.niss.website/main/niss/2024-03-14-quorientation/>
|
||||||
|
<img src=../images/quorientation.png>
|
||||||
|
</a>
|
||||||
|
</figure>
|
||||||
|
|
||||||
|
in [this picture], what is q.t. saying? this:
|
||||||
|
|
||||||
|
:::{.figure .bigscr}
|
||||||
|
`{#suatł pattalal šilbari gulaigúšḿ fulla}` \
|
||||||
|
`{#sá sá panísat igitḿ ǧunailam lám ušmináša nat lánášḿ fulla}` \
|
||||||
|
`{#ǧisat fuhat siham iksaháš}`
|
||||||
|
:::
|
||||||
|
|
||||||
|
so. one sentence at a time.
|
||||||
|
|
||||||
|
[this picture]: http://gallery.niss.website/main/niss/2024-03-14-quorientation/
|
||||||
|
|
||||||
|
# one
|
||||||
|
|
||||||
|
:::glosses
|
||||||
|
- suatł pattalal šilbari gulaigúšḿ fulla
|
||||||
|
- [ˌsuətɫ̩ ˈpatːɐləlʲ ˈʃilʲbɐɾɪ ɡɔˈlaɪɣɔːʃm̩ fʊɫːɑ]
|
||||||
|
- sua-t-ł patta-la-l šil-ba-ri gulai-gúš-ḿ fulla
|
||||||
|
- 2-GEN-PL door-INS-PL floor-SUP-PRL jump-2p can
|
||||||
|
- use your warps to skip some floors
|
||||||
|
:::
|
||||||
|
|
||||||
|
you know! the thing! from the game!
|
||||||
|
|
||||||
|
<figure class='floating right'>
|
||||||
|
<figcaption> well. from the fan translation </figcaption>
|
||||||
|
<img src=../images/skip-some-floors.png class=pixel alt=''>
|
||||||
|
</figure>
|
||||||
|
|
||||||
|
- out of context, `{!patta}` means door. i suppose a portal would be a magic
|
||||||
|
door, an `{!ustaitł patta}`. but in the context of someone making one right
|
||||||
|
in front of you, it is clear what kind of door we're talking about.
|
||||||
|
|
||||||
|
:::{.aside .no-line}
|
||||||
|
the word `{!ustail}` also means "songs". did you know there's an old english
|
||||||
|
word for magic, `{ġealdor}`, that comes from the proto-germanic `{galdr}`,
|
||||||
|
meaning both "song" and "incantation"? i thought it was cute.
|
||||||
|
:::
|
||||||
|
|
||||||
|
- the suffix pair `{!–bari}` together mean "over". there was something like this
|
||||||
|
[last time](chrismas.html) too. since it is how the language expresses all
|
||||||
|
spatial and temporal relationships, that's not very surprising.
|
||||||
|
|
||||||
|
# two
|
||||||
|
|
||||||
|
:::glosses
|
||||||
|
- sá sá panísat igitḿ ǧunailam lám ušmináša nat lánášḿ fulla
|
||||||
|
- [saːsɐ pɐˈniːsɐt ˈiʝɛtm̩ dʒuˈnaɪlɐ̃ ˌlãːm‿ʊʃmiˈnaːʃə ˌnat ˈlaːnaːʃm̩ ˌfʊɫːə]
|
||||||
|
- sá_sá panísa-t igi(s)-t-ḿ ǧunai-la-m lá-m ušmi-náš-(j)a na(i)-t lá-náš-ḿ fulla
|
||||||
|
- now blue-GEN crystal-GEN-DEF rod-INS-DEF do-DEF want-1p-REL one-GEN do-1p-DEF can
|
||||||
|
- these days we can use the blue crystal rod for whatever we want
|
||||||
|
:::
|
||||||
|
|
||||||
|
babylon no longer exists, so it doesn't need protecting. go have fun
|
||||||
|
|
||||||
|
- one `{!sá}` means "right at this moment". two `{!sá sá}` means "these days".
|
||||||
|
the second one is actually pronounced with a short vowel.
|
||||||
|
|
||||||
|
- `{!igis}` also means "ice". "crystal" more explicitly can be `{!kut igis}`,
|
||||||
|
or "stone ice".
|
||||||
|
|
||||||
|
- `{!nai}` means both "one" and "anything". phrased more literally,
|
||||||
|
`{!lám ušmináša nat}` is "anything that we want to do".
|
||||||
|
|
||||||
|
- the way auxiliary verbs like "can" work is a little strange. let's take
|
||||||
|
a shorter sentence, `{!šanil gubam fulla}`, "flowers can grow". first you take
|
||||||
|
the base sentence, `{!šanil guba}` "flowers grow", and add `{m}`, which
|
||||||
|
when it's not part of a grammatical template, means "the", but makes the
|
||||||
|
clause into a noun phrase. then that is used as the subject of the verb
|
||||||
|
`{!fulla}`, or `{!bulla}` "must", etc. so more literally, these auxiliaries
|
||||||
|
mean something like "is possible/necessary".
|
||||||
|
"{flowers grow here} is possible".
|
||||||
|
|
||||||
|
:::{.aside .no-line}
|
||||||
|
the similarity of `{!fulla}` and `{!bulla}` is just a weird accident, in case
|
||||||
|
you're wondering. i made the words at different times. no etymology puzzle
|
||||||
|
here, sorry
|
||||||
|
:::
|
||||||
|
|
||||||
|
# three
|
||||||
|
|
||||||
|
:::glosses
|
||||||
|
- ǧisat fuhat siham iksaháš
|
||||||
|
- [ˈdʒisɐt ˌfuxɑt ˈsixɑ̃m‿ˌiksɐxɑːʃ]
|
||||||
|
- ǧisa-t fuha-t siha-m iksa-háš
|
||||||
|
- fire-GEN breath-GEN remember-DEF IMP-2p
|
||||||
|
- be careful with the fire breath
|
||||||
|
:::
|
||||||
|
|
||||||
|
- `{!iksa}` has the same grammatical structure as `{!fulla}` above. it makes a
|
||||||
|
sentence into a request. it has one special feature: since in the
|
||||||
|
vast majority of cases, it only makes sense for both `{!iksa}` and the main
|
||||||
|
verb to be second person, when that _is_ the case, only `{!iksa}` needs to
|
||||||
|
have the person marking. otherwise it would be `{!sihaham}` above.
|
||||||
|
|
||||||
|
# abbreviation list
|
||||||
|
|
||||||
|
:::{.twocol .abbr-list}
|
||||||
|
DEF
|
||||||
|
: [definite](https://lang.niss.website/laantas/nouns.html#definiteness)
|
||||||
|
["the"]{.note}
|
||||||
|
|
||||||
|
GEN
|
||||||
|
: [genitive](https://lang.niss.website/laantas/nouns.html#corecases)
|
||||||
|
["of"]{.note}
|
||||||
|
|
||||||
|
INS
|
||||||
|
: [instrumental](https://lang.niss.website/laantas/nouns.html#corecases)
|
||||||
|
["using"]{.note}
|
||||||
|
|
||||||
|
PL
|
||||||
|
: [plural](https://lang.niss.website/laantas/nouns.html#number)
|
||||||
|
|
||||||
|
PRL
|
||||||
|
: [perlative](https://lang.niss.website/laantas/nouns.html#locational-cases)
|
||||||
|
["through"]{.note}
|
||||||
|
|
||||||
|
REL
|
||||||
|
: [relative clause suffix](https://lang.niss.website/laantas/verbs.html#modifier-forms)
|
||||||
|
["which/that"]{.note}
|
||||||
|
|
||||||
|
SUP
|
||||||
|
: [superessive](https://lang.niss.website/laantas/nouns.html#locational-cases)
|
||||||
|
["above"]{.note}
|
||||||
|
:::
|
||||||
Loading…
Reference in a new issue