125 lines
6.1 KiB
Plaintext
125 lines
6.1 KiB
Plaintext
---
|
||
title: advent of code 2023, day 1
|
||
...
|
||
|
||
|
||
since this is a brand new language, we need to define… quite a lot.
|
||
|
||
|
||
## booleans
|
||
|
||
enumerations are one of the base kinds of type in quox. an enumeration type looks like `{a, b, c, …}` and the values look like `'a`.
|
||
|
||
```quox
|
||
namespace bool {
|
||
|
||
def0 Bool : ★ = {true, false}
|
||
```
|
||
|
||
one of the things quox's type system does is keep track of how many times each variable is used. it's like a much simpler version of rust's Whole Situation. i think something nice can be built on top of it, but that's in the future. anyway, this extends a little bit to top-level definitions: if something is marked `0`, then it doesn't exist at all at run time. this is needed for types, which have no run time representation, but can also be used for anything else that shouldn't exist when the compiler is done, like correctness proofs, or whatever.
|
||
|
||
`1` on the type of a function argument (or no marker, since it's the default) means it is used exactly once in all code paths. `ω` means it can be used however you like. the two branches of `if` below are `ω`, because whether they are used or not depends on the value of `b`, and saying that exactly is not possible (currently??). the default for top level definitions is `ω`, since it doesn't make much sense to have one that can be used once, ever, _somewhere_.
|
||
|
||
you match against enums (and most other things) with a `case` expression. currently, the return type annotation is mandatory, because it can't _always_ be inferred, and the machinery to figure it out when it _is_ possible doesn't exist yet.
|
||
|
||
```quox
|
||
def if : 0.(A : ★) → (b : Bool) → ω.A → ω.A → A =
|
||
λ A b t f ⇒ case b return A of { 'true ⇒ t; 'false ⇒ f }
|
||
|
||
def and : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a b 'false
|
||
def or : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a 'true b
|
||
|
||
} -- (end of namespace)
|
||
```
|
||
|
||
<aside>
|
||
`and` and `or` here are just normal functions that evaluate both their arguments. sorry.
|
||
</aside>
|
||
|
||
for the same reason as the `return` annotation, there's no inference for type arguments and stuff like that, so the type of `if`'s branches has to be specified as the first argument.yes this is annoying. it'll be gone one day.
|
||
|
||
there's also no module importing yet, so if i want to use a name unqualified i just bind it again outside of a namespace for now. without getting Into It, a single name is one of the things whose types is obvious enough not to need an annotation (and type constructors aren't. if you know you know).
|
||
|
||
```quox
|
||
def0 Bool = bool.Bool
|
||
```
|
||
|
||
unit, or `()`, or whatever you want to call it, is an even simpler enumeration. since it has no useful information, it can be thrown away, but not automatically yet.
|
||
|
||
```quox
|
||
namespace unit {
|
||
def0 Unit : ★ = {unit}
|
||
|
||
def drop : 0.(A : ★) → A → Unit → A =
|
||
λ A x u ⇒ case u return A of { 'unit ⇒ x }
|
||
}
|
||
|
||
def0 Unit = unit.Unit
|
||
```
|
||
|
||
|
||
## maybe (aka option)
|
||
|
||
booleans are all right, but what if you need data _inside_ your data.
|
||
|
||
quox's enums are _just_ the symbols, so instead, you can use a pair. the first element is your enum, and the second element is everything else. what that is depends on the tag, so we write a function `Payload` that returns the type we need. `Nothing` needs no thing (well, a placeholder), and `Just` needs one thing.
|
||
|
||
```quox
|
||
namespace maybe {
|
||
|
||
def0 Tag : ★ = {nothing, just}
|
||
|
||
def0 Payload : Tag → ★ → ★ =
|
||
λ tag A ⇒ case tag return ★ of { 'nothing ⇒ Unit; 'just ⇒ A }
|
||
|
||
def0 Maybe : ★ → ★ =
|
||
λ A ⇒ (t : Tag) × Payload t A
|
||
|
||
def Nothing : 0.(A : ★) → Maybe A = λ A ⇒ ('nothing, 'unit)
|
||
def Just : 0.(A : ★) → A → Maybe A = λ A x ⇒ ('just, x)
|
||
```
|
||
|
||
with the language in this early state it's easier to work types if we define folds for them. for today, non-dependent versions will do, like haskell's `maybe` or rust's `map_or`. and if i make it take the two components separately, i can put off talking about the `x` of quox until another day.
|
||
|
||
```quox
|
||
def fold' : 0.(A B : ★) → ω.B → ω.(ω.A → B) →
|
||
ω.(tag : Tag) → ω.(Payload tag A) → B =
|
||
λ A B nothing just tag ⇒
|
||
case tag return t ⇒ ω.(Payload t A) → B of {
|
||
'nothing ⇒ λ _ ⇒ nothing;
|
||
'just ⇒ λ x ⇒ just x
|
||
}
|
||
|
||
def fold : 0.(A B : ★) → ω.B → ω.(ω.A → B) → ω.(Maybe A) → B =
|
||
λ A B nothing just x ⇒
|
||
caseω x return B of { (tag, payload) ⇒ fold' A B nothing just tag payload }
|
||
|
||
}
|
||
|
||
def0 Maybe = maybe.Maybe
|
||
def Just = maybe.Just
|
||
def Nothing = maybe.Nothing
|
||
```
|
||
|
||
it is possible to make these types more precise about how they use their arguments, but let's worry about that some other time. this is good enough for now.
|
||
|
||
`fold'` looks a bit weird here. first, its return annotation has an extra `t ⇒` at the beginning. and it also has a pattern match before it's taken all of its arguments, so the arms inside the case are both functions. sorry i lied there are dependent types afoot on the inside of this function
|
||
|
||
first let's try to write it like this:
|
||
|
||
```{.quox}
|
||
def fold' : 0.(A B : ★) → ω.B → ω.(ω.A → B) →
|
||
ω.(tag : Tag) → ω.(Payload tag A) → B =
|
||
λ A B nothing just tag payload ⇒
|
||
case tag return B of {
|
||
'nothing ⇒ nothing;
|
||
'just ⇒ just payload
|
||
}
|
||
```
|
||
|
||
in the second branch, the type of `just` is `ω.A → B`, and the type of `payload` is `Payload tag A`. right now, the type system can't see that these are the same, so you get an error. but in this branch, `tag` is `'just`, so `payload` _should_ have type `Payload 'just A`, which is `A`. to make this connection obvious, you can write a return clause as `return x ⇒ T`, which means that, in each branch, occurrences of `x` will be replaced with that branches pattern, and for the whole expression's type, they will be replaced with the head. this is also the reason for matching before taking the last argument: it is the occurrence in that argument's type that we care about.
|
||
|
||
maybe you are thinking "the word `tag` is right there! of course i want to replace it!" and in future versions of the language simple examples like this will be more automatic. but for now cut me some slack ok
|
||
|
||
|