# Injectivity

## 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!!

-}

```