Injectivity

Table of Contents

• Introduction
• Potential Problems
• Bigger Example

Introduction

If F is injective and the type checker knows that F i = F j it could conclude i = j to solve further constraints. For examples if F is a name of an inductive family or a constructor, it is injective. If F is defined then it is not injective in general, but in some important cases it is. For instance, define Vectors by recursion.

data Nat where
  zero : Nat
  suc  : Nat -> Nat

data Empty where

data Prod (A B : Set) : Set where
    pair : A -> B -> Prod A B

Vec : (A : Set) -> Nat -> Set
Vec A zero     = Empty
Vec A (succ n) = Prod A (Vec A n)

Vec is an injective function, which can be shown by induction on Nat. I guess in this case injectivity could be statically checked. It would be nice to be able to specify that a function is injective (via a pragma), and this way get more support from the type checker.

Potential problems

Consider the following set of equations:

Vec A ?0 = Vec A ?1
?1 = succ zero

Given the injectivity trick, we could solve these equations by first instantiating ?0 := ?1 and then ?1 := succ zero. Now, suppose we tried to solve the equations is the reverse order. We'd end up with the constraint Vec A ?0 = Prod A Empty which we can't solve with just the injectivity trick. There are two options:

• Never solve the constraints. For instance, by requiring that one side is neutral when applying injectivity.
• Always solve the constraints. This would be a bit trickier. Faced with the constraint Vec A ?0 = Prod A Empty we would have to figure out that this could only happen in the succ case and instantiate ?0 := succ ?2.

Bigger Example

Here is a bigger example, comparing two implementations of a type, one by induction, one by recursion.

module RecVsData where

-- empty type

data Empty : Set where

-- natural numbers

data Nat : Set where
  Zero : Nat
  Succ : Nat -> Nat

-- vectors

data Vec (A : Set) : Nat -> Set where
  []   : Vec A Zero
  _::_ : forall {n} -> A -> Vec A n -> Vec A (Succ n)

infixr 20 _::_

map : {A B : Set} -> (A -> B) -> forall {n} -> Vec A n -> Vec B n
map f [] = []
map f (x :: xs) = f x :: map f xs 

-- Sized types, variables: i

Size = Nat


-- First coding of kinds, via an inductive datatype

module KindData where

  data Kind : {_ : Size} -> Set where
    mkKind : forall {i n} -> Vec (Kind {i}) n -> Kind {Succ i}

  wkKind : forall { i } -> Kind { i } -> Kind { Succ i }
  wkKind { Succ i } (mkKind ks) = mkKind (map wkKind ks)


-- Second coding of kinda, via recursion

module KindRec where

  data MkKind (K : Set) : Set  where
    mkKind : forall { n } -> Vec K n -> MkKind K

  Kind : {_ : Size} -> Set 
  Kind { Zero }   = Empty
  Kind { Succ i } = MkKind (Kind {i})

  wkKind : forall { i } -> Kind { i } -> Kind { Succ i }
  wkKind { Zero   } ()
  wkKind { Succ i } (mkKind ks) = mkKind (map wkKind ks)
  -- THREE UNSOLVED MVARS HERE
  -- RESOLVED IF INSTEAD:  mkKind (map (wkKind { i }) ks)
  -- A RECORD INSTEAD Of MkKind DOES NOT SOLVE THE PROBLEM

{- Manual type-checking

  LHS    ks  =>  Vec (Kind { i }) ?1

  Check  mkKind (map wkKind ks) <= Kind { Succ (Succ i) }
                                 = MkKind (Kind { Succ i })

  Check  map wkKind ks          <= Vec (Kind { Succ i }) ?2

  Infer  map => forall {A B n} -> (A -> B) -> Vec A n -> Vec B n

  Check  wkKind     <= A -> B
  Infer  wkKind ?3  => Kind { ?3 } -> Kind { Succ ?3 }

  Infer  map wkKind => Vec (Kind { ?3 }) ?4 -> Vec (Kind { Succ ?3 }) ?4

  Check  ks         <= Vec (Kind { ?3 }) ?4

  Solve  ?3 = i     Probably this setting is not performed, since Kind def.by.rec.
         ?4 = ?1

  Infer  map wkKind ks => Vec (Kind { Succ ?3 }) ?1
  Solve  ?2 = ?1

  If one would rely on the *injectivity* of Kind, then 
  the setting ?3 = i could be made!!

-}