From a248240a6a98cad5178ae2f14c369d03ba176fad Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Thu, 30 Mar 2023 03:29:11 -0500 Subject: [PATCH] more on induction + implement language switcher --- assets/sass/_content.scss | 75 ++++++++- content/posts/2023-03-26-inductive-types.md | 164 ++++++++++++++++++-- layouts/_default/baseof.html | 2 +- layouts/posts/single.html | 21 +++ layouts/shortcodes/language-switcher.html | 28 ++++ 5 files changed, 277 insertions(+), 13 deletions(-) create mode 100644 layouts/shortcodes/language-switcher.html 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 }} +
+{{ end }} +
diff --git a/layouts/shortcodes/language-switcher.html b/layouts/shortcodes/language-switcher.html new file mode 100644 index 0000000..4c4c0ae --- /dev/null +++ b/layouts/shortcodes/language-switcher.html @@ -0,0 +1,28 @@ +{{ $_hugo_config := `{ "version": 1 }` }} + +{{ $parts := split .Inner "---" }} +{{ $page := .Page }} + +
+ +
    +{{ range $index, $snippet := $parts }} + {{ $lang := index $page.Params.language_switcher_languages $index }} +
  • + +
    • +{{ end }} +
+ + +
+ {{ range $index, $snippet := $parts }} +
+ {{ $snippet | markdownify }} +
+ {{ end }} +
+ +
+ +{{/* Thank you https://codepen.io/MPDoctor/pen/mpJdYe */}}