Dependent types: enforcing global properties in inductive types

4
votes

I have the following inductive type MyVec:

import Data.Vect

data MyVec: {k: Nat} -> Vect k Nat -> Type where
  Nil: MyVec []
  (::): {k, n: Nat} -> {v: Vect k Nat} -> Vect n Nat -> MyVec v -> MyVec (n :: v)

-- example:
val: MyVec [3,2,3]
val = [[2,1,2], [0,2], [1,1,0]]

That is, the type specifies the lengths of all vectors inside a MyVec.

The problem is, val will have k = 3 (k is the number of vectors inside a MyVec), but the ctor :: does not know this fact. It will first build a MyVec with k = 1, then with 2, and finally with 3. This makes it impossible to define constraints based on the final shape of the value.

For example, I cannot constrain the values to be strictly less than k. Accepting Vects of Fin (S k) instead of Vects of Nat would rule out some valid values, because the last vectors (the first inserted by the ctor) would "know" a smaller value of k, and thus a stricter contraint.

Or, another example, I cannot enforce the following constraint: the vector at position i cannot contain the number i. Because the final position of a vector in the container is not known to the ctor (it would be automatically known if the final value of k was known).

So the question is, how can I enforce such global properties?

1
dependent-typeidris

1 Answers

4
votes

There are (at least) two ways to do it, both of which may require tracking additional information in order to check the property.

Enforcing properties in the data definition

Enforcing all elements < k

I cannot constrain the values to be strictly less than k. Accepting Vects of Fin (S k) instead of Vects of Nat would rule out some valid values...

You are right that simply changing the definition of MyVect to have Vect n (Fin (S k)) in it would not be correct.

However, it is not too hard to fix this by generalizing MyVect to be polymorphic, as follows.

data MyVec: (A : Type) -> {k: Nat} -> Vect k Nat -> Type where
  Nil: {A : Type} -> MyVec A []
  (::): {A : Type} -> {k, n: Nat} -> {v: Vect k Nat} -> Vect n A -> MyVec A v -> MyVec A (n :: v)

val : MyVec (Fin 3) [3,2,3]
val = [[2,1,2], [0,2], [1,1,0]]

The key to this solution is separating the type of the vector from k in the definition of MyVec, and then, at top level, using the "global value of k to constrain the type of vector elements.

Enforcing vector at position i does not contain i

I cannot enforce that the vector at position i cannot contain the number i because the final position of a vector in the container is not known to the constructor.

Again, the solution is to generalize the data definition to keep track of the necessary information. In this case, we'd like to keep track of what the current position in the final value will be. I call this index. I then generalize A to be passed the current index. Finally, at top level, I pass in a predicate enforcing that the value does not equal the index.

data MyVec': (A : Nat -> Type) -> (index : Nat) -> {k: Nat} -> Vect k Nat -> Type where
  Nil: {A : Nat -> Type} -> {index : Nat} -> MyVec' A index []
  (::): {A : Nat -> Type} -> {k, n, index: Nat} -> {v: Vect k Nat} ->
        Vect n (A index) -> MyVec' A (S index) v -> MyVec' A index (n :: v)

val : MyVec' (\n => (m : Nat ** (n == m = False))) 0 [3,2,3]
val = [[(2 ** Refl),(1 ** Refl),(2 ** Refl)], [(0 ** Refl),(2 ** Refl)], [(1 ** Refl),(1 ** Refl),(0 ** Refl)]]

Enforcing properties after the fact

Another, sometimes simpler way to do it, is to not enforce the property immediately in the data definition, but to write a predicate after the fact.

Enforcing all elements < k

For example, we can write a predicate that checks whether all elements of all vectors are < k, and then assert that our value has this property.

wf : (final_length : Nat) -> {k : Nat} -> {v : Vect k Nat} -> MyVec v -> Bool
wf final_length [] = True
wf final_length (v :: mv) = isNothing (find (\x => x >= final_length) v) && wf final_length mv

val : (mv : MyVec [3,2,3] ** wf 3 mv = True)
val = ([[2,1,2], [0,2], [1,1,0]] ** Refl)

Enforcing vector at position i does not contain i

Again, we can express the property by checking it, and then asserting that the value has the property.

wf : (index : Nat) -> {k : Nat} -> {v : Vect k Nat} -> MyVec v -> Bool
wf index [] = True
wf index (v :: mv) = isNothing (find (\x => x == index) v) && wf (S index) mv

val : (mv : MyVec [3,2,3] ** wf 0 mv = True)
val = ([[2,1,2], [0,2], [1,1,0]] ** Refl)