Numbering Matters: First-Order Canonical Forms for Second-Order Recursive Types

Nadji Gauthier - François Pottier

Motivation

• Object encodings typically require polymorphism and recursive types

Isorecursive  Equirecursive
\overline{fold τ[μα.τ/α] : μα.τ} \overline{unfold μα.τ : τ[μα.τ/α]} μα.τ = τ[μα.τ/α]

• Most(all?) encodings use isorecursive types, and is not challenging from an equality testing point of view

Roadmap

• F_{μ} syntax

• Notion of equality

• Highlight of the difficulties

• Related work

• Reduction of equality testing from second order to first order • Conclusion F_{μ} syntax

\begin{aligned}τ & := & α \\ & | & a \\ & | & τ → τ \\ & | & ∀a.τ \\ & | & μα.τ \end{aligned}

• quantification only binds atoms • atoms are integers

F_{μ} type example

τ,syntax  τ, graphical  ⟦τ⟧

μα.∀a.a → α  \begin{aligned}& ∀a \\ & → \\ a \end{aligned}  ∀a → a \begin{aligned}& ∀a \\ & → \\ a \end{aligned}

• τ =_{2o} τ′ equal by definition to ⟦τ⟧ = ⟦τ′⟧ • The formal definition of =_{2o} is by coinduction • Problem : given τ, τ′, is ⟦τ⟧ = ⟦τ′⟧ ?

The difference with first order equality

∀a → β  ∀b → a  ≠_{2o}  ^{∀a → β  ∀b → a  ∀a → β}

• If we don’t interpret these types modulo α-conversion, those two types are equal

• But the scope of binders does not extend through back edges, we need to α-convert in order to unfold the right type

∀a → β  ∀b → a ^{∀a → β  ∀b → a} ≠_{2o}  ^{∀a → β  ∀b → a  ∀c → β  ∀b → a}

Related work

• Colazzo and Ghelli [1] decide Kernel F_{≤} subtyping (!)

• Glew’s [2] algorithm in O(n^{2})

• These results are not directly applicable to unification, entailment ...

• We propose O(n log n)

Deciding equality between second order types In order to check if two universally quantified types are equal, we need

to perform a renaming :

∀a.τ =^{?} ∀b.τ′ ⇔ τ =^{?} (τ′[b/a]), a ∉ fa(τ′)

• Renaming is costly, we would like to avoid it

• in System F, it is possible with De Bruijn encoding :

∀.τ =^{?} ∀.τ′ ⇔ τ =^{?} τ′

• we want an encoding such that τ =_{2o} τ′ ⇔ enc(τ) =_{1o} enc(τ′)

Cycles and the De Bruijn encoding

\begin{matrix}A & B & C & D \\ _{∀a → a  ∀b^{a → ∀b}} & _{∀a → a  ∀b} & _{∀ → 0  ∀} & _{∀ → 0  ∀^{1 → ∀}} \end{matrix}

• C is the encoding of B, B unfolds to A, C unfolds to D

• But D is not a first order unfolding of C

First order target syntax

\begin{aligned}σ & := & α \\ & | & a \\ & | & σ → σ \\ & | & μα.σ \\ & | & ∀_{a}.σ \end{aligned}  \begin{aligned}Q & : & σ → τ \\ Q(α) & = & α \\ Q(a) & = & a \\ Q(σ_{1} → σ_{2}) & = & Q(σ_{1}) → Q(σ_{2}) \\ Q(μα.σ) & = & μα.Q(σ) \\ Q(∀_{a}.σ) & = & ∀a.Q(σ) \end{aligned}

• ∀_{1}.1 ≠_{1o} ∀_{2}.2

• Q is the decoding function, it simply takes the quotient modulo alpha conversion on atoms indexed by ∀_{a} constructors

• Q(∀_{1}.1) = ∀a.a = Q(∀_{2}.2)

Encoding

\begin{matrix}A & B & C & D \\ ∀a → a  ∀b^{a → ∀b} & ^{∀a → a ∀a} & ^{∀_{1} → 1  ∀_{1}} & ∀_{1} → 1  ∀_{1}^{1 → ∀_{1}} \end{matrix}

• Unfolding C at first order and then decoding does not give back A

∀a → a  ∀b^{a → ∀b}  ^{∀a → a ∀a}  ^{∀_{1} → 1  ∀_{2}}  ∀_{1} → 1  ∀_{2}^{1 → ∀_{2}}

• We want first order unfolding to imitate second order unfolding • unfolding then encoding must be equivalent to encoding then unfold-

ing

Encoding example (1)

∀a → a  ∀b

∀a → a  ∀b ∅ {a}

∀_{1} → 1  ∀b {1}

∀_{1} → 1  ∀_{2}

• We choose the first order constructor relatively to the infinite tree below its node

• Thus, two equal types will have the same constructor

• The choice depends on the free atoms of the infinite tree, and this property is invariant by unfolding

∀a → β  ∀b → a  ^{∀a → β  ∀b → a  ∀a → β}

∀a → β  ∀b → a ∅ {a}  ^{∀a → β  ∀b → a  ∀a → β}

∀_{1} → β  ∀b → 1 {1}  ^{∀a → β  ∀b → a  ∀a → β}

∀_{1} → β  ∀_{2} → 1  ^{∀a → β  ∀b → a  ∀a → β}

∀_{1} → β  ∀_{2} → 1  ^{∀a → β  ∀b → a  ∀c → β}

∀_{1} → β  ∀_{2} → 1  ∀a → β  ∀b → a  ∀c → β ∅ {a} {a}

∀_{1} → β  ∀_{2} → 1  ∀_{1} → β  ∀b → 1  ∀c → β {1} {1}

∀_{1} → β  ∀_{2} → 1  ∀_{1} → β  ∀_{2} → 1  ∀c → β {1}

∀_{1} → β  ∀_{2} → 1  ^{∀_{1} → β  ∀_{2} → 1  ∀_{2} → β}

Conclusion

• encoding an F_{μ} type can be done in O(n log n)

• similar reductions exists for the unification and entailment problem • generalizable to other binding constructs

• compatible with rows

• http://pauillac.inria.fr/~gauthier/

References

[1] D. Colazzo and G. Ghelli. Subtyping recursive types in kernel fun. In IEEE Symposium on Logic in Computer Science (LICS), pages 137–146, July 1999.

[2] N. Glew. A theory of second-order trees. In European Symposium on Programming (ESOP), volume 2305 of Lecture Notes in Computer Science, pages 147–161. Springer Verlag, Apr. 2002.