# Refining types

In dependently typed programming, I find it’s common to start with some “imprecise” type and refine it to something that contains more information. For example, I might receive a `String`

from user input and want to turn that into a `Vect n Char`

(for some given `n`

) when I write proofs about my code:

```
fromString : String
-> (n : Nat ** Vect n Char)
```

Generally this refinement is accompanied by proofs that the refinement was correct. For instance, we might want to show that length is preserved:

```
lengthPreserved : (s : String)
-> getWitness (fromString s) = length s
```

and use this to build a copy of the refined value with the existential unpacked:

```
fromString' : (s : String) -> Vect (length s) Char
fromString' s = let prf = lengthPreserved s in
rewrite sym prf in
getProof $ fromString s
```

**Exercise**: Implement `fromString`

and `lengthPreserved`

.

This factorization of `fromString'`

into the simpler components of `lengthPreserved`

and `fromString`

makes you wonder if this process can be generalized. To start off this generalization, we are looking for a function that takes `length`

and the two components and produces `fromString'`

:

```
fromString' : (length : String -> Nat)
-> (fromString : String -> (n : Nat ** Vect n Char))
-> (lengthPreserved : (s : String) -> getWitness (fromString s) = length s)
-> (s : String)
-> Vect (length s) Char
```

Generalizing the dependent pair to the `Sigma`

typeclass (and making the substitution `Vect' n = Vect n Char`

), we get:

```
fromString' : (length : String -> Nat)
-> (fromString : String -> Sigma Nat Vect')
-> (lengthPreserved : (s : String) -> getWitness (fromString s) = length s)
-> (s : String)
-> Vect' (length s)
```

and we’re basically there. Now, all that’s left is to parameterize on our unrefined type `String`

, our refined type `Vect'`

, and its index the `Nat`

(along with some generous renaming and re-arranging):

```
sko : {a b : Type}
-> { pred : b -> Type }
-> (iexists : a -> Sigma b pred)
-> (f : a -> b)
-> (witness : (s : a) -> getWitness (iexists s) = f s)
-> (s : a)
-> p (f s)
```

Now, to figure out what this thing really is, let’s turn to the Curry-Howard interpretation of it, going parameter by parameter:

`iexists : a -> Sigma b t`

If we think of `a`

as an index, this describes an indexed family of existence proofs on the predicate `pred`

, with witnesses taking type `a`

.

`f : a -> b`

`f`

tells us that `a`

can be interpreted as something other than an index, by relating it to `b`

.

`(witness : (s : a) -> getWitness (iexists s) = f s)`

Now, `f`

has been related to the existence proofs by being identical to the witness over `a`

. This tells us that `f`

perfectly describes the witnesses of the indexed family `iexists`

.

`(s : a) -> p (f s)`

Given all these conditions, we can think of this as a new family of indexed proofs, except the witness has been replaced with a transformation of `f`

. The existential type has been eliminated and replaced with a universally quantified type instead.

Now, whenever we want to prove that a refinement into another type has a certain property, we don’t have to do it all in one go. We also don’t have to worry about unpacking existentials afterwards. Curiously, this process looks a lot like skolemization.