From 608503637c2dbde17ba7ab2564aa2995b7601e02 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Wed, 29 Mar 2023 15:03:10 -0500 Subject: [PATCH] inductive types wip --- .build.yml | 16 -- .woodpecker.yml | 2 +- assets/sass/_content.scss | 29 +++- assets/sass/main.scss | 2 +- content/posts/2023-03-26-inductive-types.md | 154 ++++++++++++++++++++ 5 files changed, 182 insertions(+), 21 deletions(-) delete mode 100644 .build.yml create mode 100644 content/posts/2023-03-26-inductive-types.md diff --git a/.build.yml b/.build.yml deleted file mode 100644 index 222d5a5..0000000 --- a/.build.yml +++ /dev/null @@ -1,16 +0,0 @@ -image: archlinux -packages: - - hugo - - rsync -secrets: - - 0b26b413-7901-41c3-a4e2-3c752228ffcb -sources: - - https://git.sr.ht/~mzhang/blog -tasks: - - build: | - cd blog - hugo --buildDrafts --minify --baseURL https://mzhang.io - - upload: | - cd blog - echo "mzhang.io ssh-ed25519 AAAAC3NzaC1lZDI1NTE5AAAAIBzBZ+QmM4EO3Fwc1ZcvWV2IY9VF04T0H9brorGj9Udp" >> ~/.ssh/known_hosts - rsync -azvrP public/ sourcehutBuilds@mzhang.io:/mnt/storage/svcdata/blog-public diff --git a/.woodpecker.yml b/.woodpecker.yml index 02f4ae2..c9a3c12 100644 --- a/.woodpecker.yml +++ b/.woodpecker.yml @@ -2,7 +2,7 @@ pipeline: build: image: klakegg/hugo:ext-pandoc-ci commands: - - hugo --minify --baseURL https://mzhang.io + - hugo --buildDrafts --minify --baseURL https://mzhang.io deploy: image: alpine diff --git a/assets/sass/_content.scss b/assets/sass/_content.scss index e16130a..e88a78d 100644 --- a/assets/sass/_content.scss +++ b/assets/sass/_content.scss @@ -14,7 +14,7 @@ html { } body { - max-width: 980px; + max-width: 1024px; margin: auto; width: 100%; height: 1px; @@ -262,7 +262,7 @@ code { box-sizing: border-box; padding: 1px 5px; background-color: $faded-background-color; - color: $code-color; + // color: $code-color; } a code { @@ -315,7 +315,7 @@ table.table { .post-title { font-size: 2rem; font-weight: 500; - margin-bottom: 0; + margin-bottom: 12px; } .tags { @@ -380,6 +380,29 @@ table.table { } min-width: 1px; + + details { + border: 1px solid lightgray; + padding: 10px 30px; + font-size: 0.9rem; + } + + hr { + border-width: 1px 0 0 0; + border-color: $faded-background-color; + margin: 32px auto; + width: 20%; + } + + .highlight { + .lntd:first-child { + // border-right: 1px solid lightgray; + padding-right: 2px; + } + .lntd:last-child { + padding-left: 12px; + } + } } &.logseq-post { diff --git a/assets/sass/main.scss b/assets/sass/main.scss index 91d058e..1c547d7 100644 --- a/assets/sass/main.scss +++ b/assets/sass/main.scss @@ -29,7 +29,7 @@ $monofont: "PragmataPro Mono Liga", "Roboto Mono", "Roboto Mono for Powerline", @media (prefers-color-scheme: dark) { $background-color: #202030; - $faded-background-color: lighten($background-color, 10%); + $faded-background-color: lighten($background-color, 30%); $shadow-color: lighten($background-color, 10%); $heading-color: lighten(lightskyblue, 20%); $text-color: #CDCDCD; diff --git a/content/posts/2023-03-26-inductive-types.md b/content/posts/2023-03-26-inductive-types.md new file mode 100644 index 0000000..5ea781b --- /dev/null +++ b/content/posts/2023-03-26-inductive-types.md @@ -0,0 +1,154 @@ ++++ +title = "Inductive Types" +slug = "inductive-types" +date = 2023-03-26 +tags = ["type-theory"] +math = true +draft = true ++++ + +There's a feature common to many functional languages, the ability to have +algebraic data types. It might look something like this (OCaml syntax): + +```ocaml +type bool = +| True +| False +``` + +For those who are unfamiliar with the syntax, I'm defining a type called `bool` +that has two _constructors_, or ways to create this type. The constructors are +`True` and `False`. This means: + +1. Any time I use the value `True`, it's understood to have type `bool`. +2. Any time I use the value `False`, it's understood to have type `bool`. +3. In addition, there are _no_ other ways to create values of `bool` other than combining `True` and `False` constructors. + +--- + +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. + +Now, in type theory, one of the interesting things to know about a type is its +_cardinality_. For example, the type `Boolean` is defined to have cardinality 2. +That's because there's only one constructor, so if at any point you have some +unknown value of type `Boolean`, you know it can only take one of two values. + +
+ Note about Booleans + +There's actually nothing special about boolean itself. I could just as easily +define a new type, like this: + +```ocaml +type WeirdType = +| Foo +| 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`. + +I would have to define my own operators such as AND and OR separately, but +those aren't properties of the `Boolean` type itself, they are properties of +the Boolean algebra, which has several [algebraic properties][1] such as +associativity, commutativity, distributivity, and several others. Think of it +as a sort of _interface_, where if you can implement that interface, your type +qualifies as a Boolean algebra! + +[1]: https://en.wikipedia.org/wiki/Boolean_algebra_(structure)#Definition + +
+ +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: + +```ocaml +type unit = +| Unit +``` + +There's only one way to ever construct something of this type, so the +cardinality of this type would be 1. + +## Doing Things with Types + +Creating types and making values of those data types is just the first part +though. It would be completely uninteresting if all we could do is create types. +So, the way we typically use these types is through _pattern matching_ (also +called structural matching in some languages). + +Let's see an example. Suppose I have a type with three values, defined like +this: + +```ocaml +type direction = +| Left +| Middle +| Right +``` + +If I was given a value with type `direction`, but I wanted to do different +things depending on exactly which direction it was, I could use _pattern +matching_ like this: + +```ocaml +let do_something_with (d : direction) = + match d with + | Left -> do_this_if_left + | Middle -> do_this_if_middle + | Right -> do_this_if_right +``` + +This gives me a way to discriminate between the different variants of +`direction`. + +> Most languages have a built-in construct for discriminating between values 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 + +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 +but those, it would be very painful to write in! This is where _type +constructors_ come in. + +When I say type constructor, I mean a type that can take types and build other +types out of them. There's several ways this can be done, but the one I want to +discuss today is called _inductive_ types. + +> If you don't know what induction is, the [Wikipedia article][2] on it is a +> great place to start! +> +> [2]: https://en.wikipedia.org/wiki/Mathematical_induction + +The general idea is that we can build types using either base cases (variants +that don't contain themselves as a type), or inductive cases (variants that _do_ +contain themselves as a type). + +You can see an example of this here: + +```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: + +```ocaml +let is_even = fun (x : nat) -> + match x with + | Suc n -> not (is_even n) + | Zero -> true +```