Functional pearl:

From concrete to functional unparsing

Jean-François Monin

Verimag

Université Joseph Fourier

Grenoble

Work started at SRI (thanks to N. Shankar and J. Rushby)

TPHOLS’04, Park City, Utah, 14-17 sept 2004

What this talk is about

Format = string (C, Ocaml...)

sprintf ("The %s is %d %s.", "distance", 10, "meters")
"The distance is 10 meters."

Format = structured value (e.g. list)

[Lit("The "); String; [Lit(" is "); Int; String; [Lit(".")]

Format = function (Danvy, Functional Unparsing)

lit "The " o string o lit " is " o int o string o lit "."

• user extensible

• dynamic evaluation of formats is allowed

Why does it work?

Functional formats (Danvy)

let int k s x = k (s ^string_of_int x)

(string → α) → string → int → α

let str k s x = k (s ^x)

(string → α) → string → string → α

let lit x k s = k (s ^x)

string → (string → α) → string → α

let sprintf f = f λs.s ""

General pattern: (string → α) → string → […] → α

Damas-Milner typing

In general, the type of a functional format has the form (string → α) → string → X_{1} → ⋯ → X_{n} → α. If two formats f_{1} and f_{2} are respectively of type

(string → β) → string → X_{1} → ⋯ → X_{n} → β

and

(string → α) → string → X_{n+1} → ⋯ → X_{n+p} → α

then their composition f_{1} ∘ f_{2} is of type (string → α) → string → X_{1} → ⋯ → X_{n} → X_{n+1} → ⋯ → X_{n+p} → α

Goal

Show that sprintf and sprintfk have exactly the same behavior Given a concrete format ϕ, define the corresponding functional format kformat ϕ Theorem sprintf sprintfk:

∀ϕ sprintf ϕ = sprintfk (kformat ϕ).

Features of the formalization

Type system • inductive types (concrete formats)

• polymorphism (functional formats, Damas-Milner)

• higher order, higher order types (Damas-Milner)

• dependent types, computed types ⇒ CIC (Coq) Methodological points

• extensionality/intensionality

• functional pattern recognition

Part 1: Typing formats

Concrete formats (1)

Record Printable : Type := mkpr

{X : Set ; r X : string → X → string }. appends to the right Type format :=

| Stop | Data of Printable × format | Lit of string × format.

example := Lit foo (Str (Lit bar (Int Stop))). "foo %s bar %i" Fixpoint type of fmt ϕ : Set :=

match ϕ with | Stop ⇒ string | Data P ϕ ⇒ X P → type of fmt ϕ | Lit s ϕ ⇒ type of fmt ϕ end.

type of fmt example reduces to string → int → string.

Concrete formats (2)

Fixpoint type of fmt ϕ : Set := match ϕ with | Stop ⇒ string | Data P ϕ ⇒ X P → type of fmt ϕ | Lit s ϕ ⇒ type of fmt ϕ end.

Fixpoint r sprintf ϕ : string → type of fmt ϕ := match ϕ with | Stop ⇒ λa. a | Data P ϕ ⇒ λa x. r sprintf ϕ (a _{ P̂} x) | Lit s ϕ ⇒ λa. r sprintf ϕ (a ˆ s) end.

Definition sprintf ϕ := r sprintf ϕ "".

Untyped functional formats

Definition sprintfk := λf. f (λs. s) "".

Definition kid := λk a. k a. Definition kdata P := λα. λk. λa x. k (a _{ P̂} x). Definition lit (x:string) := λα. λk a. k (aˆ x).

Fixpoint kformat ϕ := match ϕ with | Stop ⇒ kid | Data P ϕ ⇒ (kdata P) ∘ (kformat ϕ) | Lit x ϕ ⇒ (lit x) ∘ (kformat ϕ) end.

kformat example is convertible with (lit foo) ∘ (kdata Str) ∘ (lit bar) ∘ (kdata Int) (lit foo) ∘ str ∘ (lit bar) ∘ sint

Typing functional formats (1)

kid : (string →string) → string → string

kdata P : ∀α (string →α) → string → X P → α

lit (x:string) : ∀α (string →α) → string → α

Fixpoint kformat ϕ : (string → string ) → string → type of fmt ϕ := match ϕ with | Stop ⇒ kid | Data P ϕ ⇒ (kdata P (type of fmt ϕ)) ∘ (kformat ϕ) | Lit x ϕ ⇒ (lit x (type of fmt ϕ)) ∘ (kformat ϕ) end.

kformat example is convertible with (lit foo (string →int →string)) ∘ (str (int →string)) ∘ (lit bar (int →string)) ∘ (sint string ).

This is unfair!

If ϕ is a given closed format, the expression kformat ϕ has a closed type as well. (kformat (Lit foo (Str Stop))) ∘ (kformat (Lit bar (Int Stop))) is ill-typed.

We want Damas-Milner

Type transformers (1)

λα. etc → … → etc → α

of type : Set →Set

Forget type of fmt, use type transf of fmt instead.

Type transformers (2)

Definition idt := λα. α. Definition datat P := λα. (X P → α).

Fixpoint type transf of fmt ϕ : Set →Set := match ϕ with | Stop ⇒ idt | Data P ϕ ⇒ (datat P) ∘ (type transf of fmt ϕ) | Lit s ϕ ⇒ type transf of fmt ϕ end.

Fixpoint r sprintf ϕ : string →type transf of fmt ϕ string := match ϕ with | Stop ⇒ λa. a | Data P ϕ ⇒ λa x. r sprintf ϕ (a _{ P̂} x) | Lit s ϕ ⇒ λa. r sprintf ϕ (a ˆ s) end.

Typing functional formats (3)

The type given to a functional format takes the form kt tf , where tf is a type transformer. Definition kt (tf : Set → Set ) := ∀α (string → α) → string → tf α. Definition kid : kt idt := λα. λk a. k a. Definition kdata P : kt (λα. X P → α) :=

λα. λk : string →α. λa x. k (a _{ P̂} x). Definition lit x : kt idt := λα. λk a. k (aˆ x). Specialized version of function composition: Definition u seq (tg, tf : Set → Set ) : kt tg → kt tf → kt (tg ∘ tf) :=

λg f. λα. λk. g (tf α) (f α k). Notation: g ⊚ f

Typing functional formats (4)

Definition sprintfk (tf : Set → Set ) : kt tf → tf string := λf. f string (λs. s) "".

Fixpoint kformat ϕ : kt (type transf of fmt ϕ) := match ϕ with | Stop ⇒ kid | Data P ϕ ⇒ (kdata P) ⊚ (kformat ϕ) | Lit x ϕ ⇒ (lit x) ⊚ (kformat ϕ) end.

Formats can be composed

kformat example convertible with (kformat (Lit foo (Str Stop))) ⊚ (kformat (Lit bar (Int Stop)))

Part 2: Correctness proof Correctness of sprintfk w.r.t. sprintf

∀ϕ sprintf ϕ = sprintfk (kformat ϕ)

First attempt : ∀ϕ r sprintf ϕ "" = kformat ϕ (λs. s) "" the accumulator changes at each recursive call prove something on "" ˆ s while the induction hypothesis is on ""

Generalize: ∀a r sprintf ϕ a = kformat ϕ (λs. s) a

Subgoal:

λx. r sprintf ϕ (a _{ P̂} x) = λx. kformat ϕ string (λs. s) (a _{ P̂} x)

We are stuck!

Use extensionality?

∀α β, ∀f g : α → β, (∀x:α, f x = g x) → (λx. f x) = (λx. g x)

Avoid axioms!

Try a weaker statement

Instead of

∀a r sprintf ϕ a = kformat ϕ (λs. s) a

consider a more extensional statement:

∀a ∀v, r sprintf ϕ a v = kformat ϕ (λs. s) a v

Can be done, but heavy, ugly and… too weak

Try a stronger statement

Instead of

∀a r sprintf ϕ a = kformat ϕ (λs. s) a

consider a more intensional statement:

λa. r sprintf ϕ a = λa. kformat ϕ (λs. s) a

Subgoal:

λaλx. r sprintf ϕ (a _{ P̂} x) = λaλx. kformat ϕ string (λs. s) (a _{ P̂} x) Eureka : f ∘_{2} g := λx y. f (g x y)

λaλx. f (a _{ P̂} x) = (λa. f a) ∘_{2} (r X P)

(λa. r sprintf ϕ a) ∘_{2} (r X P) = (λa. kformat ϕ (λs. s) a) ∘_{2} (r X P) QED

By chance, eta-reduction works here

Instead of

λa. r sprintf ϕ a = λa. kformat ϕ (λs. s) a

consider the (stronger) statement:

r sprintf ϕ = kformat ϕ (λs. s)

Subgoal:

λaλx. r sprintf ϕ (a _{ P̂} x) = λaλx. kformat ϕ string (λs. s) (a _{ P̂} x) QED

Reminder

Type system • inductive types (concrete formats)

• polymorphism (functional formats)

• higher order, higher order types • dependent types, computed types

⇒ CIC (Coq) Methodological points

• extensionality/intensionality

• functional pattern recognition

Conclusion

ACL2-like slogan

No functional pearl too trivial No extensional proof too obscure