mirror of
https://github.com/Brandon-Rozek/website.git
synced 2024-09-19 06:05:14 -04:00
96 lines
2.3 KiB
Markdown
96 lines
2.3 KiB
Markdown
---
|
||
title: "Polymorphic Functions w/ Wildcard Matching in Lean 4"
|
||
date: 2024-08-04T07:21:07-07:00
|
||
draft: false
|
||
tags: []
|
||
math: false
|
||
medium_enabled: false
|
||
---
|
||
|
||
I was reading through the [Polymorphism](https://lean-lang.org/functional_programming_in_lean/getting-to-know/polymorphism.html) section in the Functional programming in Lean textbook and came across the following example:
|
||
|
||
```lean4
|
||
inductive Sign where
|
||
| pos
|
||
| neg
|
||
|
||
def posOrNegThree (s : Sign) : match s with | Sign.pos => Nat | Sign.neg => Int :=
|
||
match s with
|
||
| Sign.pos => (3 : Nat)
|
||
| Sign.neg => (-3 : Int)
|
||
```
|
||
|
||
The function `posOrNegThree` depending on the input, can either return an expression of type `Nat` or an expression of type `Int`. That's super neat!
|
||
|
||
What happens if we add a wildcard to the match?
|
||
|
||
For example, let's say we want a type based on the number of bits of precision specified. If we don't support the number of bits, we return the arbitrary precision `Nat` as our default.
|
||
|
||
```lean4
|
||
def UIntN (n: Nat) : Type := match n with
|
||
| 32 => UInt32
|
||
| 64 => UInt64
|
||
| _ => Nat
|
||
```
|
||
|
||
Now let's write a function that returns the zero element of our specified type:
|
||
|
||
```lean4
|
||
def u0 (x: Nat) : UIntN x := match x with
|
||
| 32 => (0: UInt32)
|
||
| 64 => (0: UInt64)
|
||
| _ => Nat.zero
|
||
```
|
||
|
||
This will result in the following error:
|
||
|
||
```lean4
|
||
type mismatch
|
||
Nat.zero
|
||
has type
|
||
ℕ : Type
|
||
but is expected to have type
|
||
UIntN x✝ : Type
|
||
```
|
||
|
||
I got stuck on this for a while, so I asked on the really helpful Lean Zulip and got a [great response](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20Polymorphic.20Functions.20w.2F.20Wildcard.20Match.20Type)
|
||
|
||
```lean4
|
||
def u0 (x: Nat) : UIntN x := dite (x=32) (λ h ↦ by
|
||
subst h
|
||
exact (0 : UInt32)
|
||
) (dite (x = 64) (λ h ↦ by
|
||
intro h2
|
||
subst h
|
||
exact (0: UInt64)
|
||
)
|
||
(λ h ↦ by
|
||
intro h2
|
||
have : UIntN x = Nat := by
|
||
unfold UIntN
|
||
simp only
|
||
rw [this]
|
||
exact 0
|
||
))
|
||
```
|
||
|
||
Unfortunately this doesn't look pretty, but this was a massive clue in finding the prettier syntax to solve this problem!
|
||
|
||
```lean4
|
||
def u0 (x: Nat) : UIntN x :=
|
||
if h: x = 6 then by
|
||
subst h
|
||
exact (0: UInt32)
|
||
else if h2: x = 4 then by
|
||
subst h2
|
||
exact (0: UInt64)
|
||
else by
|
||
have : UIntN x = Nat := by
|
||
unfold UIntN
|
||
simp only
|
||
rw [this]
|
||
exact 0
|
||
```
|
||
|
||
|
||
|