diff --git a/chrismas.md b/chrismas.md deleted file mode 100644 index 5115e74..0000000 --- a/chrismas.md +++ /dev/null @@ -1,189 +0,0 @@ - - - - - - - - - - -
-

merr chrismas

-
-

monday 25 december 2023

- -
-
-
- - -
-# just tell me how to say it please - -sure thing. here. - -```{=html} -
-``` - ---------------------------------------------------------------------- ---------------------------------------------------- - ![](chrismas/ufit_þulkussarim.svg "ufit þulkussarim"){.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} -
-``` -# 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 [![](chrismas/igisim.svg "igisim"){.scr .laantas}]{.lang} [igisim]{.lang} [\[ˈiʝɛsĩ\]]{.ipa .ipa-narrow} the freeze - feb [![](chrismas/susurum.svg "susurum"){.scr .laantas}]{.lang} [susurum]{.lang} [\[ˈsusʊrõ\]]{.ipa .ipa-narrow} the melt - mar--may [![](chrismas/šangubam.svg "šangubam"){.scr .laantas}]{.lang} [šangubam]{.lang} [\[ˈʃaŋɡɔvɑ̃\]]{.ipa .ipa-narrow} the bloom - jun--aug [![](chrismas/guwanḿ.svg "guwanḿ"){.scr .laantas}]{.lang} [guwanḿ]{.lang} [\[ˈɡɔwɑnm̩\]]{.ipa .ipa-narrow} the sun - sep--oct [![](chrismas/santum.svg "santum"){.scr .laantas}]{.lang} [santum]{.lang} [\[ˈsantõ\]]{.ipa .ipa-narrow} the rain - -- in between [![](chrismas/igisim.svg "igisim"){.scr - .laantas}[igisim]{.text}]{.lang} (winter) and - [![](chrismas/šangubam.svg "šangubam"){.scr - .laantas}[šangubam]{.text}]{.lang} (spring), the month of february - is considered a transition between the two, - [![](chrismas/susurum.svg "susurum"){.scr - .laantas}[susurum]{.text}]{.lang}. -- as a result, [![](chrismas/santum.svg "santum"){.scr - .laantas}[santum]{.text}]{.lang} (autumn) is only two months long. -- [![](chrismas/šangubam.svg "šangubam"){.scr - .laantas}[šangubam]{.text}]{.lang} comes from - [![](chrismas/šani.svg "šani"){.scr .laantas}[šani]{.text}]{.lang} - (flower) and [![](chrismas/guba.svg "guba"){.scr - .laantas}[guba]{.text}]{.lang} (grow, thrive). - -## putting it together - -the word "midwinter", without any inflections, is -[![](chrismas/þulkusim.svg "þulkusim"){.scr -.laantas}[þulkusim]{.text}]{.lang}, which comes from -[![](chrismas/þulku.svg "þulku"){.scr .laantas}[þulku]{.text}]{.lang} -"be deep" and [![](chrismas/igisim.svg "igisim"){.scr -.laantas}[igisim]{.text}]{.lang}. unusually for lántas, -[![](chrismas/þulku.svg "þulku"){.scr .laantas}[þulku]{.text}]{.lang} is -a verb, rather than a noun. why? who knows. - -```{=html} - -``` -the suffix [![](chrismas/–sari.svg "–sari"){.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 -[![](chrismas/–m.svg "–m"){.scr .laantas}[--m]{.text}]{.lang} on the end -(of all these words so far, actually) is "the". so the full form -[![](chrismas/þulkusisarim.svg "þulkusisarim"){.scr -.laantas}[þulkusisarim]{.text}]{.lang} means "during midwinter", and -that one [i]{.lang} is dropped in this phrase to give the form -[![](chrismas/þulkussarim.svg "þulkussarim"){.scr -.laantas}[þulkussarim]{.text}]{.lang}. - -now, for [![](chrismas/ufit.svg "ufit"){.scr -.laantas}[ufit]{.text}]{.lang}. there is a small, but technically -non-zero, chance that you remember the word -[![](chrismas/uf_a_t.svg "uf{a}t"){.scr -.laantas}[uf``{=html}a``{=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 -[![](chrismas/iksaha.svg "iksaha"){.scr -.laantas}[iksaha]{.text}]{.lang}, like before. this is an auxiliary verb -for requests. for example, if [![](chrismas/šikkúha.svg "šikkúha"){.scr -.laantas}[šikkúha]{.text}]{.lang} means "you are going", then -[![](chrismas/šikkúm_iksaha.svg "šikkúm iksaha"){.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 -[![](chrismas/ufit_þulkussarim.svg "ufit þulkussarim"){.scr -.laantas}[ufit þulkussarim]{.text}]{.lang}, meaning "\[stay\] cozy -during the midwinter". - -::: twocol-grid -![](images/crismas1.png){width="100%"} - -```{=html} -
-``` - ---------------------------------------------------------- ---- - ![](chrismas/þugusim_ai.svg "þugusim ai"){.scr .laantas} - þugusim ai - \[ˈθuɣɔsĩm‿ai\] - þugusi--m ai - miwiner--[DEF]{.abbr} be - it crismas - ---------------------------------------------------------- ---- - -```{=html} -
-``` -![](images/crismas2.png){width="100%"} - -```{=html} -
-``` - ------------------------------------------------------------------ ---------------------------------------- - ![](chrismas/ufi_þugussarim.svg "ufi þugussarim"){.scr .laantas} - ufi þugussarim - \[ˌufi ˈθuɣɔsːɐʑĩ\] - ufi--(t) þugus(i)--sari--m - cozy--([GEN]{.abbr}) miwiner--[DURING]{.abbr}--[DEF]{.abbr} - merr crismas - ------------------------------------------------------------------ ---------------------------------------- - -```{=html} -
-``` -::: - -
- - - - diff --git a/images/quorientation.png b/images/quorientation.png new file mode 100644 index 0000000..8af38fb Binary files /dev/null and b/images/quorientation.png differ diff --git a/images/skip-some-floors.png b/images/skip-some-floors.png new file mode 100644 index 0000000..f5601dd Binary files /dev/null and b/images/skip-some-floors.png differ diff --git a/posts-wip/2023-10-25-quox.md.old b/posts-wip/2023-10-25-quox.md.old deleted file mode 100644 index 536dd69..0000000 --- a/posts-wip/2023-10-25-quox.md.old +++ /dev/null @@ -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 -... - - - - -:::{.aside .floating} -### [hot minute](https://en.wiktionary.org/wiki/hot_minute) n. {.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} - -
- a dragon from an old arcade game -
this is also a quox.
-
- -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 - -
-
one of my fursonas is a quox with three heads
-
- sometimes i am also a quox. or three, depending on how you count. -
-
- -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} diff --git a/posts-wip/2023-06-12-algorithmic-xtt.md b/posts-wip/algorithmic-xtt.md similarity index 100% rename from posts-wip/2023-06-12-algorithmic-xtt.md rename to posts-wip/algorithmic-xtt.md diff --git a/posts-wip/qpoly.md b/posts-wip/qpoly.md new file mode 100644 index 0000000..02bf7b5 --- /dev/null +++ b/posts-wip/qpoly.md @@ -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} +$$ +::: diff --git a/posts-wip/record.md b/posts-wip/record.md new file mode 100644 index 0000000..b728c27 --- /dev/null +++ b/posts-wip/record.md @@ -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} +$$ diff --git a/posts/ats.md b/posts/ats.md index f98e4d7..47d46d7 100644 --- a/posts/ats.md +++ b/posts/ats.md @@ -3,6 +3,8 @@ title: a little ats program date: 2022-09-16 tags: [computer, ATS, cool languages] 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 @@ -60,9 +62,7 @@ let's start by defining the syntax for types. it's going to be a single base type, and functions. $$ -\newcommand\Typ{\mathit{typ}} -\newcommand\OR{\mathrel|} -\Typ ::= \bullet \OR \Typ_1 \to \Typ_2 +A, B \operatorname{::=} \mathord• \mid A → B $$ 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 application. -$$ -\newcommand\Term{\mathit{term}} -\newcommand\Var{\mathit{var}} -\Term ::= \Var \OR \lambda \Var : \Typ. \Term \OR \Term_1 \; \Term_2 -$$ +$$ s, t \operatorname{::=} x \mid λ x : A. s \mid s \; t $$ 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 diff --git a/posts/beluga.md b/posts/beluga.md index 9e44cc2..4cf4c62 100644 --- a/posts/beluga.md +++ b/posts/beluga.md @@ -3,6 +3,9 @@ date: 2022-07-12 title: a few undocumented beluga features tags: [computer, beluga, cool languages] toc: true +summary: | + some undocumented features i found while looking through the source code + of the proof language beluga. ... diff --git a/posts/chrismas.md b/posts/chrismas.md index 53b6150..08cfb13 100644 --- a/posts/chrismas.md +++ b/posts/chrismas.md @@ -3,6 +3,11 @@ date: 2023-12-25 title: merr chrismas tags: [lántas, conlangs] 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 @@ -74,7 +79,7 @@ so in the end, you get `{!ufit þulkusimsari}`, meaning "[stay] cozy during the midwinter". -:::twocol-grid +::: {.twocol-grid .light} ![](images/crismas1.png){width=100%} ::: {.glosses .left} diff --git a/posts/digitle-in-maude.md b/posts/digitle-in-maude.md index 88351a4..cdd92a9 100644 --- a/posts/digitle-in-maude.md +++ b/posts/digitle-in-maude.md @@ -2,6 +2,9 @@ title: digitle in maude date: 2022-03-14 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. diff --git a/posts/fib.md b/posts/fib.md index 923f0cf..14b3e2c 100644 --- a/posts/fib.md +++ b/posts/fib.md @@ -2,6 +2,8 @@ title: fibonacci in maude and ats date: 2022-10-24 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. diff --git a/posts/idris2-features.md b/posts/idris2-features.md index 9c76ea6..a9c2352 100644 --- a/posts/idris2-features.md +++ b/posts/idris2-features.md @@ -2,6 +2,10 @@ title: undocumented idris2 features date: 2022-11-12 tags: [computer, idris] +summary: | + some lesser-known features in the dependently-typed language + idris (2). + header-includes: |