blog/src/content/posts/2023-10-10-dtt-project.lagda.md

title	date	draft	toc	tags
DTT Project	2023-10-11T04:05:23.082Z	true	true	type-theory

References:

• https://www.cl.cam.ac.uk/~nk480/bidir.pdf

Agda Imports for the purpose of type-checking

{-# OPTIONS --allow-unsolved-metas --allow-incomplete-matches #-}
open import Data.Nat
open import Data.Product
open import Data.String hiding (_<_)
open import Relation.Nullary using (Dec)
open import Relation.Nullary.Decidable using (True; toWitness)

Damas-Hindley-Milner type inference

Unification-based algorithm for lambda calculus.

First try

Implement terms, monotypes, and polytypes:

data Term : Set
data Type : Set
data Monotype : Set

Regular lambda calculus terms:

e ::= x \mid () \mid \lambda x. e \mid e e \mid (e : A)

data Term where
    Unit : Term
    Var : String → Term
    Lambda : String → Term → Term
    App : Term → Term → Term
    Annot : Term → Type → Term

Polytypes are types that may include universal quantifiers ($\forall$)

A, B, C ::= 1 \mid \alpha \mid \forall \alpha. A \mid A \rightarrow B

data Type where
    Unit : Type
    Var : String → Type
    Existential : String → Type
    Forall : String → Type → Type
    Arrow : Type → Type → Type

Monotypes (usually denoted $\tau$) are types that aren't universally quantified.

[!NOTE] In the declarative version of this algorithm, monotypes don't have existential quantifiers either, but the algorithmic type system includes it. TODO: Explain why

data Monotype where
    Unit : Monotype
    Var : String → Monotype
    Existential : String → Monotype
    Arrow : Monotype → Monotype → Monotype

Contexts

data Context : Set where
    Nil : Context
    Var : Context → String → Context
    Annot : Context → String → Type → Context
    UnsolvedExistential : Context → String → Context
    SolvedExistential : Context → String → Monotype → Context
    Marker : Context → String → Context

contextLength : Context → ℕ
contextLength Nil = zero
contextLength (Var Γ _) = suc (contextLength Γ)
contextLength (Annot Γ _ _) = suc (contextLength Γ)
contextLength (UnsolvedExistential Γ _) = suc (contextLength Γ)
contextLength (SolvedExistential Γ _ _) = suc (contextLength Γ)
contextLength (Marker Γ _) = suc (contextLength Γ)

-- https://plfa.github.io/DeBruijn/#abbreviating-de-bruijn-indices
postulate
    lookupVar : (Γ : Context) → (n : ℕ) → (p : n < contextLength Γ) → Set
-- lookupVar (Var Γ x) n p = {!   !}
-- lookupVar (Annot Γ x x₁) n p = {!   !}
-- lookupVar (UnsolvedExistential Γ x) n p = {!   !}
-- lookupVar (SolvedExistential Γ x x₁) n p = {!   !}
-- lookupVar (Marker Γ x) n p = {!   !}

data CompleteContext : Set where
    Nil : CompleteContext
    Var : CompleteContext → String → CompleteContext
    Annot : CompleteContext → String → Type → CompleteContext
    SolvedExistential : CompleteContext → String → Monotype → CompleteContext
    Marker : CompleteContext → String → CompleteContext

Type checking

postulate
    check : (Γ : Context) → (e : Term) → (A : Type) → Context

-- check Γ Unit A = Γ

-- check Γ (Var x) A = {!   !}
-- check Γ (Lambda x e) A = {!   !}
-- check Γ (App e e₁) A = {!   !}
-- check Γ (Annot e x) A = {!   !}

Type synthesizing

const x = () => {};

postulate
    synthesize : (Γ : Context) → (e : Term) → (Type × Context)
-- synthesize Γ Unit = Unit , Γ
-- synthesize Γ (Var x) = {!   !}
-- synthesize Γ (Lambda x e) = {!   !}
-- synthesize Γ (App e e₁) = {!   !}
-- synthesize Γ (Annot e x) = {!   !}