diff --git a/assets/sass/_content.scss b/assets/sass/_content.scss
index e88a78d..ecb0644 100644
--- a/assets/sass/_content.scss
+++ b/assets/sass/_content.scss
@@ -338,6 +338,73 @@ table.table {
}
}
+// Tabbing
+.language-switcher-choice {
+ display: none;
+}
+
+.tabbed {
+ border: 1px solid #eee;
+
+ ul.tabs {
+ margin-top: 0;
+ margin-bottom: 0;
+ list-style: none;
+ padding-inline-start: 0;
+ border-bottom: 1px solid lightgray;
+
+ .tab {
+ display: inline-block;
+ list-style: none;
+
+ label {
+ display: inline-block;
+ padding: 4px 8px;
+ font-size: 0.9rem;
+ }
+ }
+ }
+
+ .contents {
+ .tab-content {
+ padding: 0 12px;
+
+ &:not(:last-child) {
+ border-bottom: 1px solid gray;
+ }
+ }
+ }
+}
+
+@for $i from 1 through 5 {
+ $colors: [green, red, blue, yellow, purple];
+
+ .language-switcher-choice:nth-of-type(#{$i}):checked {
+ outline: 2px solid nth($colors, $i);
+ }
+
+ body:has(.language-switcher-choice:nth-of-type(#{$i}):checked) .tabbed {
+ .tabs .tab:nth-child(#{$i}) {
+ border-bottom: 3px solid gray;
+ }
+
+ .tabs .tab:not(:nth-child(#{$i})) {
+ border-bottom: 3px solid transparent;
+ }
+
+ .contents .tab-content:nth-child(#{$i}) {
+ border-bottom: none;
+ }
+
+ .contents .tab-content:not(:nth-child(#{$i})) {
+ // text-shadow: 2px 2px nth($colors, $i);
+ display: none;
+ }
+ }
+}
+
+// Post container
+
.post-container {
display: flex;
@@ -375,7 +442,7 @@ table.table {
*/
.post-content {
- ul {
+ ul:not(.tabs) {
padding-left: 1.5rem;
}
@@ -403,6 +470,12 @@ table.table {
padding-left: 12px;
}
}
+
+ .highlight,
+ details {
+ margin-top: 16px;
+ margin-bottom: 16px;
+ }
}
&.logseq-post {
diff --git a/content/posts/2023-03-26-inductive-types.md b/content/posts/2023-03-26-inductive-types.md
index 5ea781b..90c5ac2 100644
--- a/content/posts/2023-03-26-inductive-types.md
+++ b/content/posts/2023-03-26-inductive-types.md
@@ -1,15 +1,17 @@
+++
title = "Inductive Types"
-slug = "inductive-types"
date = 2023-03-26
tags = ["type-theory"]
math = true
draft = true
+
+language_switcher_languages = ["ocaml", "python"]
+++
There's a feature common to many functional languages, the ability to have
-algebraic data types. It might look something like this (OCaml syntax):
+algebraic data types. It might look something like this:
+{{< language-switcher >}}
```ocaml
type bool =
| True
@@ -26,6 +28,20 @@ that has two _constructors_, or ways to create this type. The constructors are
---
+```python
+from typing import Literal
+MyBool = Literal[True] | Literal[False]
+```
+{{}}
+
+> **Note:** I'm using an experimental language switcher. It's implemented in
+> pure CSS using a feature called the [`:has` pseudo-class][has]. As of writing,
+> all major browsers _except_ Firefox has it implemented and enabled by default.
+> For Firefox there does exist a feature flag in about:config, but your mileage
+> may vary.
+
+---
+
Many languages have this feature, under different names. Tagged unions, variant
types, enumerations, but they all reflect a basic idea: a type with a limited
set of variants.
@@ -41,12 +57,21 @@ unknown value of type `Boolean`, you know it can only take one of two values.
There's actually nothing special about boolean itself. I could just as easily
define a new type, like this:
+{{< language-switcher >}}
```ocaml
type WeirdType =
| Foo
| Bar
```
+---
+
+```python
+from typing import Literal
+WeirdType = Literal['foo'] | Literal['bar']
+```
+{{}}
+
Because this type can only have two values, it's _semantically_ equivalent to
the `Boolean` type. I could use it anywhere I would typically use `Boolean`.
@@ -65,11 +90,20 @@ You can make any _finite_ type like this: just create an algebraic data type
with unit constructors, and the result is a type with a finite cardinality. If I
wanted to make a unit type for example:
+{{< language-switcher >}}
```ocaml
type unit =
| Unit
```
+---
+
+```python
+from typing import Literal
+Unit = Literal[None]
+```
+{{}}
+
There's only one way to ever construct something of this type, so the
cardinality of this type would be 1.
@@ -83,6 +117,7 @@ called structural matching in some languages).
Let's see an example. Suppose I have a type with three values, defined like
this:
+{{< language-switcher >}}
```ocaml
type direction =
| Left
@@ -90,10 +125,19 @@ type direction =
| Right
```
-If I was given a value with type `direction`, but I wanted to do different
+---
+
+```python
+from typing import Literal
+Direction = Literal['left'] | Literal['middle'] | Literal['right']
+```
+{{}}
+
+If I was given a value with a type of direction, but I wanted to do different
things depending on exactly which direction it was, I could use _pattern
matching_ like this:
+{{< language-switcher >}}
```ocaml
let do_something_with (d : direction) =
match d with
@@ -102,6 +146,22 @@ let do_something_with (d : direction) =
| Right -> do_this_if_right
```
+---
+
+```python
+def do_something_with(d : Direction) -> str:
+ match inp:
+ case 'left': return do_this_if_left
+ case 'middle': return do_this_if_middle
+ case 'right': return do_this_if_right
+ case _: assert_never(inp)
+```
+
+**Note:** the `assert_never` is a static check for exhaustiveness. If we missed
+a single one of the cases, a static type checker like [pyright] could catch it
+and tell us which of the remaining cases there are.
+{{}}
+
This gives me a way to discriminate between the different variants of
`direction`.
@@ -109,7 +169,7 @@ This gives me a way to discriminate between the different variants of
> the `Boolean` type, called if-else. What would if-else look like if you wrote
> it as a function in this pattern-matching form?
-## The Algebra of Types
+## Constructing larger types
Finite-cardinality types like the ones we looked at just now are nice, but
they're not super interesting. If you had a programming language with nothing
@@ -131,24 +191,106 @@ contain themselves as a type).
You can see an example of this here:
+{{< language-switcher >}}
```ocaml
type nat =
| Suc of nat
| Zero
```
+{{}}
These are the natural numbers, which are defined inductively. Each number is
just represented by a data type that wraps 0 that number of times. So 3 would be
`Suc (Suc (Suc Zero))`.
-This data type is _inductive_ because the `Suc` case can contain arbitrarily
-many `nat`s inside of it. This also means that if we want to talk about writing
-any functions on `nat`, we just have to supply 2 cases instead of an infinite
-number of cases:
+At this point you can probably see why these have _infinite_ cardinality: with
+the Suc case, you can keep wrapping nats as many times as you want!
+
+One key observation here is that although the _cardinality_ of the entire type is
+infinite, it only uses _two_ constructors to build it. This also means that if
+we want to talk about writing any functions on `nat`, we just have to supply 2
+cases instead of an infinite number of cases:
```ocaml
-let is_even = fun (x : nat) ->
- match x with
- | Suc n -> not (is_even n)
+let rec is_even = fun (n : nat) ->
+ match n with
| Zero -> true
+ | Suc n1 -> not (is_even n1)
```
+
+
+ Try it for yourself
+
+ If you've got an OCaml interpreter handy, try a couple values for yourself and
+ convince yourself that this accurately represents the naturals and an even
+ testing function:
+
+ ```ocaml
+ utop # is_even Zero;;
+ - : bool = true
+ utop # is_even (Suc Zero);;
+ - : bool = false
+ ```
+
+ This is a good way of making sure the functions you write make sense!
+
+
+## Induction principle
+
+Let's express this in the language of mathematical induction. If I have any
+natural number:
+
+- If the natural number is the base case of zero, then the `is_even` relation
+ automatically evaluates to true.
+- If the natural number is a successor, invert the induction hypothesis (which is
+ what `is_even` evaluates to for the previous step, a.k.a whether or not the
+ previous natural number is even), since every even number is succeeded by
+ an odd number and vice versa.
+
+Once these rules are followed, by induction we know that `is_even` can run on
+any natural number ever. In code, this looks like:
+
+```ocaml
+let is_even
+ (n_zero : bool)
+ (n_suc : nat -> bool)
+ (n : nat)
+ : bool =
+ match n with
+ | Zero -> n_zero
+ | Suc n1 -> n_suc n1
+```
+
+where n_zero defines what to do with the zero case, and n_suc defines what to do
+with the successor case.
+
+You might've noticed that this definition doesn't actually return any booleans.
+That's because this is not actually the is_even function! This is a general
+function that turns any natural into a boolean. In fact, we can go one step
+further and generalize this to all types:
+
+```ocaml
+let nat_transformer
+ (n_zero : 'a)
+ (n_suc : 'a -> 'a)
+ (n : nat)
+ : 'a =
+ match n with
+ | Zero -> n_zero
+ | Suc n1 -> n_suc n1
+```
+
+Let's say I wanted to write a function that converts from our custom-defined nat
+type into an OCaml integer. Using this constructor, that would look something
+like this:
+
+```ocaml
+let convert_nat = nat_transformer 0 (fun x -> x + 1)
+```
+
+
+
+TODO: Talk about https://counterexamples.org/currys-paradox.html
+
+[has]: https://developer.mozilla.org/en-US/docs/Web/CSS/:has
+[pyright]: https://github.com/microsoft/pyright
diff --git a/layouts/_default/baseof.html b/layouts/_default/baseof.html
index 79727e4..4db0586 100644
--- a/layouts/_default/baseof.html
+++ b/layouts/_default/baseof.html
@@ -14,7 +14,7 @@
{{ end }}
{{ $style := resources.Get "sass/main.scss" | resources.ToCSS }}
-
+
diff --git a/layouts/posts/single.html b/layouts/posts/single.html
index 1912afa..14f6344 100644
--- a/layouts/posts/single.html
+++ b/layouts/posts/single.html
@@ -26,6 +26,27 @@
- {{ .ReadingTime }} min read
+{{ if .Params.language_switcher_languages }}
+
+ warning! your browser does not support has
+
+
+
+ {{ range $index, $lang := .Page.Params.language_switcher_languages }}
+
+ {{ end }}
+