# ~/Blog

## Brandon Rozek

PhD Student @ RPI studying Automated Reasoning in AI and Linux Enthusiast.

# Polymorphic Functions w/ Wildcard Matching in Lean 4

Published on

2 minute reading time

I was reading through the Polymorphism section in the Functional programming in Lean textbook and came across the following example:

``````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.

``````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:

``````def u0 (x: Nat) : UIntN x := match x with
| 32 => (0: UInt32)
| 64 => (0: UInt64)
| _ => Nat.zero
``````

This will result in the following error:

``````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

``````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!

``````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
``````
Was this useful? Feel free to share: Hacker News Reddit Twitter

Published a response to this? :