Dependent de Bruijn Indices

In this example, we represent program syntax terms in a type family parameterized by a list of types, representing the typing context, or information on which free variables are in scope and what their types are.

Remark: this example is based on an example in the book Certified Programming with Dependent Types by Adam Chlipala.

Programmers who move to statically typed functional languages from scripting languages often complain about the requirement that every element of a list have the same type. With fancy type systems, we can partially lift this requirement. We can index a list type with a “type-level” list that explains what type each element of the list should have. This has been done in a variety of ways in Haskell using type classes, and we can do it much more cleanly and directly in Lean.

We parameterize our heterogeneous lists by at type α and an α-indexed type β.

inductive 
HList: {α : Type v} → (α → Type u) → List α → Type (max u v)
HList {
α: Type v
α : 
Type v: Type (v + 1)
Type v} (
β: α → Type u
β : 
α: Type v
α → 
Type u: Type (u + 1)
Type u) : 
List: Type v → Type v
List 
α: Type v
α → 
Type (max u v): Type ((max u v) + 1)
Type (max u v)
  | 
nil: {α : Type v} → {β : α → Type u} → HList β []
nil  : 
HList: {α : Type v} → (α → Type u) → List α → Type (max u v)
HList 
β: α → Type u
β 
[]: List α
[]
  | 
cons: {α : Type v} → {β : α → Type u} → {i : α} → {is : List α} → β i → HList β is → HList β (i :: is)
cons : 
β: α → Type u
β 
i: α
i → 
HList: {α : Type v} → (α → Type u) → List α → Type (max u v)
HList 
β: α → Type u
β 
is: List α
is → 
HList: {α : Type v} → (α → Type u) → List α → Type (max u v)
HList 
β: α → Type u
β (
i: α
i::
is: List α
is)

We overload the List.cons notation :: so we can also use it to create heterogeneous lists.

infix:67 " :: " => 
HList.cons: {α : Type v} → {β : α → Type u} → {i : α} → {is : List α} → β i → HList β is → HList β (i :: is)
HList.cons

We similarly overload the List notation [] for the empty heterogeneous list.

notation "[" "]" => 
HList.nil: {α : Type v} → {β : α → Type u} → HList β []
HList.nil

Variables are represented in a way isomorphic to the natural numbers, where number 0 represents the first element in the context, number 1 the second element, and so on. Actually, instead of numbers, we use the Member inductive family.

The value of type Member a as can be viewed as a certificate that a is an element of the list as. The constructor Member.head says that a is in the list if the list begins with it. The constructor Member.tail says that if a is in the list bs, it is also in the list b::bs.

inductive 
Member: {α : Type} → α → List α → Type
Member : 
α: Type
α → 
List: Type → Type
List 
α: Type
α → 
Type: Type 1
Type
  | 
head: {α : Type} → {a : α} → {as : List α} → Member a (a :: as)
head : 
Member: {α : Type} → α → List α → Type
Member 
a: ?m.3739
a (
a: ?m.3739
a::
as: List ?m.3739
as)
  | 
tail: {α : Type} → {a : α} → {bs : List α} → {b : α} → Member a bs → Member a (b :: bs)
tail : 
Member: {α : Type} → α → List α → Type
Member 
a: ?m.3911
a 
bs: List ?m.3911
bs → 
Member: {α : Type} → α → List α → Type
Member 
a: ?m.3911
a (
b: ?m.3911
b::
bs: List ?m.3911
bs)

Given a heterogeneous list HList β is and value of type Member i is, HList.get retrieves an element of type β i from the list. The pattern .head and .tail h are sugar for Member.head and Member.tail h respectively. Lean can infer the namespace using the expected type.

def 
HList.get: {α : Type} → {β : α → Type u_1} → {is : List α} → {i : α} → HList β is → Member i is → β i
HList.get : 
HList: {α : Type} → (α → Type u_1) → List α → Type u_1
HList 
β: ?m.4440 → Type u_1
β 
is: List ?m.4440
is → 
Member: {α : Type} → α → List α → Type
Member 
i: ?m.4440
i 
is: List ?m.4440
is → 
β: ?m.4440 → Type u_1
β 
i: ?m.4440
i
  | 
a: β i
a::
as: HList β is✝
as, 
.head: Member i (i :: is✝)
.head => 
a: β i
a
  | 
Warning: unused variable `a`
note: this linter can be disabled with `set_option linter.unusedVariables false`
::
as: HList β is✝
as, 
.tail: {α : Type} → {a : α} → {bs : List α} → {b : α} → Member a bs → Member a (b :: bs)
.tail 
h: Member i is✝
h => 
as: HList β is✝
as.
get: {α : Type} → {β : α → Type u_1} → {is : List α} → {i : α} → HList β is → Member i is → β i
get 
h: Member i is✝
h

Here is the definition of the simple type system for our programming language, a simply typed lambda calculus with natural numbers as the base type.

inductive 
Ty: Type
Ty where
  | 
nat: Ty
nat
  | 
fn: Ty → Ty → Ty
fn : 
Ty: Type
Ty → 
Ty: Type
Ty → 
Ty: Type
Ty

We can write a function to translate Ty values to a Lean type — remember that types are first class, so can be calculated just like any other value. We mark Ty.denote as [reducible] to make sure the typeclass resolution procedure can unfold/reduce it. For example, suppose Lean is trying to synthesize a value for the instance Add (Ty.denote Ty.nat). Since Ty.denote is marked as [reducible], the typeclass resolution procedure can reduce Ty.denote Ty.nat to Nat, and use the builtin instance for Add Nat as the solution.

Recall that the term a.denote is sugar for denote a where denote is the function being defined. We call it the "dot notation".

@[reducible] def 
Ty.denote: Ty → Type
Ty.denote : 
Ty: Type
Ty → 
Type: Type 1
Type
  | 
nat: Ty
nat    => 
Nat: Type
Nat
  | 
fn: Ty → Ty → Ty
fn 
a: Ty
a 
b: Ty
b => 
a: Ty
a.
denote: Ty → Type
denote → 
b: Ty
b.
denote: Ty → Type
denote

Here is the definition of the Term type, including variables, constants, addition, function application and abstraction, and let binding of local variables. Since let is a keyword in Lean, we use the "escaped identifier" «let». You can input the unicode (French double quotes) using \f<< (for «) and \f>> (for »). The term Term ctx .nat is sugar for Term ctx Ty.nat, Lean infers the namespace using the expected type.

inductive 
Term: List Ty → Ty → Type
Term : 
List: Type → Type
List 
Ty: Type
Ty → 
Ty: Type
Ty → 
Type: Type 1
Type
  | 
var: {ty : Ty} → {ctx : List Ty} → Member ty ctx → Term ctx ty
var   : 
Member: {α : Type} → α → List α → Type
Member 
ty: Ty
ty 
ctx: List Ty
ctx → 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
ty: Ty
ty
  | 
const: {ctx : List Ty} → Nat → Term ctx Ty.nat
const : 
Nat: Type
Nat → 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
.nat: Ty
.nat
  | 
plus: {ctx : List Ty} → Term ctx Ty.nat → Term ctx Ty.nat → Term ctx Ty.nat
plus  : 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
.nat: Ty
.nat → 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
.nat: Ty
.nat → 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
.nat: Ty
.nat
  | 
app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (dom.fn ran) → Term ctx dom → Term ctx ran
app   : 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx (
.fn: Ty → Ty → Ty
.fn 
dom: Ty
dom 
ran: Ty
ran) → 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
dom: Ty
dom → 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
ran: Ty
ran
  | 
lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (dom.fn ran)
lam   : 
Term: List Ty → Ty → Type
Term (
dom: Ty
dom :: 
ctx: List Ty
ctx) 
ran: Ty
ran → 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx (
.fn: Ty → Ty → Ty
.fn 
dom: Ty
dom 
ran: Ty
ran)
  | 
«let»: {ctx : List Ty} → {ty₁ ty₂ : Ty} → Term ctx ty₁ → Term (ty₁ :: ctx) ty₂ → Term ctx ty₂
«let» : 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
ty₁: Ty
ty₁ → 
Term: List Ty → Ty → Type
Term (
ty₁: Ty
ty₁ :: 
ctx: List Ty
ctx) 
ty₂: Ty
ty₂ → 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
ty₂: Ty
ty₂

Here are two example terms encoding, the first addition packaged as a two-argument curried function, and the second of a sample application of addition to constants.

The command open Ty Term Member opens the namespaces Ty, Term, and Member. Thus, you can write lam instead of Term.lam.

open Ty Term Member
def 
add: Term [] (nat.fn (nat.fn nat))
add : 
Term: List Ty → Ty → Type
Term 
[]: List Ty
[] (
fn: Ty → Ty → Ty
fn 
nat: Ty
nat (
fn: Ty → Ty → Ty
fn 
nat: Ty
nat 
nat: Ty
nat)) :=
  
lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (dom.fn ran)
lam (
lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (dom.fn ran)
lam (
plus: {ctx : List Ty} → Term ctx nat → Term ctx nat → Term ctx nat
plus (
var: {ty : Ty} → {ctx : List Ty} → Member ty ctx → Term ctx ty
var (
tail: {α : Type} → {a : α} → {bs : List α} → {b : α} → Member a bs → Member a (b :: bs)
tail 
head: {α : Type} → {a : α} → {as : List α} → Member a (a :: as)
head)) (
var: {ty : Ty} → {ctx : List Ty} → Member ty ctx → Term ctx ty
var 
head: {α : Type} → {a : α} → {as : List α} → Member a (a :: as)
head)))

def 
three_the_hard_way: Term [] nat
three_the_hard_way : 
Term: List Ty → Ty → Type
Term 
[]: List Ty
[] 
nat: Ty
nat :=
  
app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (dom.fn ran) → Term ctx dom → Term ctx ran
app (
app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (dom.fn ran) → Term ctx dom → Term ctx ran
app 
add: Term [] (nat.fn (nat.fn nat))
add (
const: {ctx : List Ty} → Nat → Term ctx nat
const 
1: Nat
1)) (
const: {ctx : List Ty} → Nat → Term ctx nat
const 
2: Nat
2)

Since dependent typing ensures that any term is well-formed in its context and has a particular type, it is easy to translate syntactic terms into Lean values.

The attribute [simp] instructs Lean to always try to unfold Term.denote applications when one applies the simp tactic. We also say this is a hint for the Lean term simplifier.

@[simp] def 
Term.denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → ty.denote
Term.denote : 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
ty: Ty
ty → 
HList: {α : Type} → (α → Type) → List α → Type
HList 
Ty.denote: Ty → Type
Ty.denote 
ctx: List Ty
ctx → 
ty: Ty
ty.
denote: Ty → Type
denote
  | 
var: {ty : Ty} → {ctx : List Ty} → Member ty ctx → Term ctx ty
var 
h: Member ty ctx
h,     
env: HList Ty.denote ctx
env => 
env: HList Ty.denote ctx
env.
get: {α : Type} → {β : α → Type} → {is : List α} → {i : α} → HList β is → Member i is → β i
get 
h: Member ty ctx
h
  | 
const: {ctx : List Ty} → Nat → Term ctx nat
const 
n: Nat
n,   _   => 
n: Nat
n
  | 
plus: {ctx : List Ty} → Term ctx nat → Term ctx nat → Term ctx nat
plus 
a: Term ctx nat
a 
b: Term ctx nat
b,  
env: HList Ty.denote ctx
env => 
a: Term ctx nat
a.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → ty.denote
denote 
env: HList Ty.denote ctx
env + 
b: Term ctx nat
b.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → ty.denote
denote 
env: HList Ty.denote ctx
env
  | 
app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (dom.fn ran) → Term ctx dom → Term ctx ran
app 
f: Term ctx (dom✝.fn ty)
f 
a: Term ctx dom✝
a,   
env: HList Ty.denote ctx
env => 
f: Term ctx (dom✝.fn ty)
f.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → ty.denote
denote 
env: HList Ty.denote ctx
env (
a: Term ctx dom✝
a.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → ty.denote
denote 
env: HList Ty.denote ctx
env)
  | 
lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (dom.fn ran)
lam 
b: Term (dom✝ :: ctx) ran✝
b,     
env: HList Ty.denote ctx
env => fun 
x: dom✝.denote
x => 
b: Term (dom✝ :: ctx) ran✝
b.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → ty.denote
denote (
x: dom✝.denote
x :: 
env: HList Ty.denote ctx
env)
  | 
«let»: {ctx : List Ty} → {ty₁ ty₂ : Ty} → Term ctx ty₁ → Term (ty₁ :: ctx) ty₂ → Term ctx ty₂
«let» 
a: Term ctx ty₁✝
a 
b: Term (ty₁✝ :: ctx) ty
b, 
env: HList Ty.denote ctx
env => 
b: Term (ty₁✝ :: ctx) ty
b.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → ty.denote
denote (
a: Term ctx ty₁✝
a.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → ty.denote
denote 
env: HList Ty.denote ctx
env :: 
env: HList Ty.denote ctx
env)

You can show that the denotation of three_the_hard_way is indeed 3 using reflexivity.

example: three_the_hard_way.denote [] = 3
example : 
three_the_hard_way: Term [] nat
three_the_hard_way.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → ty.denote
denote 
[]: HList Ty.denote []
[] = 
3: nat.denote
3 :=
  
rfl: ∀ {α : Type} {a : α}, a = a
rfl

We now define the constant folding optimization that traverses a term if replaces subterms such as plus (const m) (const n) with const (n+m).

@[simp] def 
Term.constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
Term.constFold : 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
ty: Ty
ty → 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
ty: Ty
ty
  | 
const: {ctx : List Ty} → Nat → Term ctx nat
const 
n: Nat
n   => 
const: {ctx : List Ty} → Nat → Term ctx nat
const 
n: Nat
n
  | 
var: {ty : Ty} → {ctx : List Ty} → Member ty ctx → Term ctx ty
var 
h: Member ty ctx
h     => 
var: {ty : Ty} → {ctx : List Ty} → Member ty ctx → Term ctx ty
var 
h: Member ty ctx
h
  | 
app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (dom.fn ran) → Term ctx dom → Term ctx ran
app 
f: Term ctx (dom✝.fn ty)
f 
a: Term ctx dom✝
a   => 
app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (dom.fn ran) → Term ctx dom → Term ctx ran
app 
f: Term ctx (dom✝.fn ty)
f.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold 
a: Term ctx dom✝
a.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold
  | 
lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (dom.fn ran)
lam 
b: Term (dom✝ :: ctx) ran✝
b     => 
lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (dom.fn ran)
lam 
b: Term (dom✝ :: ctx) ran✝
b.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold
  | 
«let»: {ctx : List Ty} → {ty₁ ty₂ : Ty} → Term ctx ty₁ → Term (ty₁ :: ctx) ty₂ → Term ctx ty₂
«let» 
a: Term ctx ty₁✝
a 
b: Term (ty₁✝ :: ctx) ty
b => 
«let»: {ctx : List Ty} → {ty₁ ty₂ : Ty} → Term ctx ty₁ → Term (ty₁ :: ctx) ty₂ → Term ctx ty₂
«let» 
a: Term ctx ty₁✝
a.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold 
b: Term (ty₁✝ :: ctx) ty
b.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold
  | 
plus: {ctx : List Ty} → Term ctx nat → Term ctx nat → Term ctx nat
plus 
a: Term ctx nat
a 
b: Term ctx nat
b  =>
    match 
a: Term ctx nat
a.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold, 
b: Term ctx nat
b.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold with
    | 
const: {ctx : List Ty} → Nat → Term ctx nat
const 
n: Nat
n, 
const: {ctx : List Ty} → Nat → Term ctx nat
const 
m: Nat
m => 
const: {ctx : List Ty} → Nat → Term ctx nat
const (
n: Nat
n+
m: Nat
m)
    | 
a': Term ctx nat
a',      
b': Term ctx nat
b'      => 
plus: {ctx : List Ty} → Term ctx nat → Term ctx nat → Term ctx nat
plus 
a': Term ctx nat
a' 
b': Term ctx nat
b'

The correctness of the Term.constFold is proved using induction, case-analysis, and the term simplifier. We prove all cases but the one for plus using simp [*]. This tactic instructs the term simplifier to use hypotheses such as a = b as rewriting/simplications rules. We use the split to break the nested match expression in the plus case into two cases. The local variables iha and ihb are the induction hypotheses for a and b. The modifier ← in a term simplifier argument instructs the term simplifier to use the equation as a rewriting rule in the "reverse direction". That is, given h : a = b, ← h instructs the term simplifier to rewrite b subterms to a.

theorem 
Term.constFold_sound: ∀ {ctx : List Ty} {ty : Ty} {env : HList Ty.denote ctx} (e : Term ctx ty), e.constFold.denote env = e.denote env
Term.constFold_sound (
e: Term ctx ty
e : 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
ty: Ty
ty) : 
e: Term ctx ty
e.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → ty.denote
denote 
env: HList Ty.denote ctx
env = 
e: Term ctx ty
e.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → ty.denote
denote 
env: HList Ty.denote ctx
env := 
Goals accomplished! 🐙

  
ctx: List Ty
ty: Ty
env: HList Ty.denote ctx
e: Term ctx ty
e.constFold.denote env = e.denote env
 
Goals accomplished! 🐙

  
ctx: List Ty
ty: Ty
ctx✝: List Ty
a, b: Term ctx✝ nat
iha: ∀ {env : HList Ty.denote ctx✝}, a.constFold.denote env = a.denote env
ihb: ∀ {env : HList Ty.denote ctx✝}, b.constFold.denote env = b.denote env
env: HList Ty.denote ctx✝
plus
(match a.constFold, b.constFold with
      | const n, const m => const (n + m)
      | a', b' => a'.plus b').denote
    env =
  a.denote env + b.denote env

    
ctx: List Ty
ty: Ty
ctx✝: List Ty
a, b: Term ctx✝ nat
iha: ∀ {env : HList Ty.denote ctx✝}, a.constFold.denote env = a.denote env
ihb: ∀ {env : HList Ty.denote ctx✝}, b.constFold.denote env = b.denote env
env: HList Ty.denote ctx✝
x✝¹, x✝: Term ctx✝ nat
n✝, m✝: Nat
heq✝¹: a.constFold = const n✝
heq✝: b.constFold = const m✝
plus.h_1
(const (n✝ + m✝)).denote env = a.denote env + b.denote env
ctx: List Ty
ty: Ty
ctx✝: List Ty
a, b: Term ctx✝ nat
iha: ∀ {env : HList Ty.denote ctx✝}, a.constFold.denote env = a.denote env
ihb: ∀ {env : HList Ty.denote ctx✝}, b.constFold.denote env = b.denote env
env: HList Ty.denote ctx✝
x✝², x✝¹: Term ctx✝ nat
x✝: ∀ (n m : Nat), a.constFold = const n → b.constFold = const m → False
(a.constFold.plus b.constFold).denote env = a.denote env + b.denote env

    
ctx: List Ty
ty: Ty
ctx✝: List Ty
a, b: Term ctx✝ nat
iha: ∀ {env : HList Ty.denote ctx✝}, a.constFold.denote env = a.denote env
ihb: ∀ {env : HList Ty.denote ctx✝}, b.constFold.denote env = b.denote env
env: HList Ty.denote ctx✝
x✝¹, x✝: Term ctx✝ nat
n✝, m✝: Nat
heq✝¹: a.constFold = const n✝
heq✝: b.constFold = const m✝
plus.h_1
(const (n✝ + m✝)).denote env = a.denote env + b.denote env
ctx: List Ty
ty: Ty
ctx✝: List Ty
a, b: Term ctx✝ nat
iha: ∀ {env : HList Ty.denote ctx✝}, a.constFold.denote env = a.denote env
ihb: ∀ {env : HList Ty.denote ctx✝}, b.constFold.denote env = b.denote env
env: HList Ty.denote ctx✝
x✝², x✝¹: Term ctx✝ nat
x✝: ∀ (n m : Nat), a.constFold = const n → b.constFold = const m → False
(a.constFold.plus b.constFold).denote env = a.denote env + b.denote env
 
Goals accomplished! 🐙

    
ctx: List Ty
ty: Ty
ctx✝: List Ty
a, b: Term ctx✝ nat
iha: ∀ {env : HList Ty.denote ctx✝}, a.constFold.denote env = a.denote env
ihb: ∀ {env : HList Ty.denote ctx✝}, b.constFold.denote env = b.denote env
env: HList Ty.denote ctx✝
x✝², x✝¹: Term ctx✝ nat
x✝: ∀ (n m : Nat), a.constFold = const n → b.constFold = const m → False
plus.h_2
(a.constFold.plus b.constFold).denote env = a.denote env + b.denote env
 
Goals accomplished! 🐙