michael/blog
1
0
Fork 0
Code Issues 2 Pull requests Releases Packages 1 Wiki Activity

let's turn on the toc
All checks were successful
ci/woodpecker/push/woodpecker Pipeline was successful
Details

Browse source
This commit is contained in:
Michael Zhang 2023-03-30 03:32:41 -05:00
parent a248240a6a
commit 6d753e5250
2 changed files with 4 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
content/posts/2023-03-26-inductive-types.md
View file

@ -4,6 +4,7 @@ date = 2023-03-26
tags = ["type-theory"] tags = ["type-theory"]
math = true math = true
draft = true draft = true
toc = true
language_switcher_languages = ["ocaml", "python"] language_switcher_languages = ["ocaml", "python"]
+++ +++
@ -107,7 +108,7 @@ Unit = Literal[None]
There's only one way to ever construct something of this type, so the There's only one way to ever construct something of this type, so the
cardinality of this type would be 1. cardinality of this type would be 1.
## Doing Things with Types ## Doing things with types
Creating types and making values of those data types is just the first part 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. though. It would be completely uninteresting if all we could do is create types.
@ -160,6 +161,8 @@ def do_something_with(d : Direction) -> str:
**Note:** the `assert_never` is a static check for exhaustiveness. If we missed **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 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. and tell us which of the remaining cases there are.
[pyright]: https://github.com/microsoft/pyright
{{</ language-switcher >}} {{</ language-switcher >}}
This gives me a way to discriminate between the different variants of This gives me a way to discriminate between the different variants of
@ -293,4 +296,3 @@ let convert_nat = nat_transformer 0 (fun x -> x + 1)
TODO: Talk about https://counterexamples.org/currys-paradox.html TODO: Talk about https://counterexamples.org/currys-paradox.html
[has]: https://developer.mozilla.org/en-US/docs/Web/CSS/:has [has]: https://developer.mozilla.org/en-US/docs/Web/CSS/:has
[pyright]: https://github.com/microsoft/pyright

4
layouts/posts/single.html
View file

@ -27,10 +27,6 @@
</small> </small>
{{ if .Params.language_switcher_languages }} {{ if .Params.language_switcher_languages }}
<div class="has-warning">
warning! your browser does not support has
</div>
<div class="language_switcher_choices"> <div class="language_switcher_choices">
{{ range $index, $lang := .Page.Params.language_switcher_languages }} {{ range $index, $lang := .Page.Params.language_switcher_languages }}
<input <input