# Injectivity

## Table of Contents

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