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

minor: parameter -> index
All checks were successful
ci/woodpecker/push/woodpecker Pipeline was successful
Details

Browse source
This commit is contained in:
Michael Zhang 2023-10-24 11:02:19 -05:00
parent 396e1f5098
commit 4895546226
1 changed files with 9 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/content/posts/2023-10-23-path-induction-gadt-perspective.lagda.md
View file

@ -31,11 +31,11 @@ Like all inductive types, it comes with the typical rules used to introduce type
For more info, see [this][equality] page. For more info, see [this][equality] page.
- Formation rule - Formation rule
- Introduction rule - Term introduction rule
- Elimination rule - Term elimination rule
- Computation rule - Computation rule
There's something quite peculiar about the elimination rule in particular (commonly known as "path induction", or just $J$). There's something quite peculiar about the elimination rule for $\mathrm{Id}$ in particular (commonly known as "path induction", or just $J$).
Let's take a look at its definition, in Agda syntax: Let's take a look at its definition, in Agda syntax:
```agda ```agda
@ -77,9 +77,11 @@ data List (A : Set) : Set where
Cons : A → List A → List A Cons : A → List A → List A
``` ```
I could write functions with this, but either polymorphically (accepts `A : Set` as a parameter, with no knowledge of what the type is) or monomorphically (as a specific `List Int` or `List Bool` or something). I could write functions with this, but either [polymorphically][polymorphism] (accepts `A : Set` as a parameter, with no knowledge of what the type is) or monomorphically (as a specific `List Int` or `List Bool` or something).
What I couldn't do would be something like this: What I couldn't do would be something like this:
[polymorphism]: https://wiki.haskell.org/Polymorphism
```text ```text
sum : (A : Set) → List A → A sum : (A : Set) → List A → A
sum Int Nil = 0 sum Int Nil = 0
@ -104,10 +106,12 @@ data Message : Set → Set₁ where
F : {T : Set} → (f : String → T) → Message T F : {T : Set} → (f : String → T) → Message T
``` ```
Note that in the definition, I've moved the parameter from the left side to the right. Note that in the definition, I've moved the parameter from the left side to an [_index_][index] on the right of the colon.
This means I'm no longer committing to a fully polymorphic `A`, which is now allowed to be assigned anything freely. This means I'm no longer committing to a fully polymorphic `A`, which is now allowed to be assigned anything freely.
In particular, it's able to take different values for different constructors. In particular, it's able to take different values for different constructors.
[index]: https://agda.readthedocs.io/en/v2.6.4/language/data-types.html#indexed-datatypes
This allows me to write functions that are polymorphic over _all_ types, while still having the ability to refer to specific types. This allows me to write functions that are polymorphic over _all_ types, while still having the ability to refer to specific types.
```agda ```agda