## Learning Dependent Types

Finally it’s starting to make sense to me. According to Wikipedia “a dependent type is a type that depends on a value”. Let’s try to break this statement and try to find out the closest corresponding concept in Haskell. In Haskell, we define datatype Maybe as

data Maybe a = Just a | Nothing.

What are the values that can be substituted for *a*? The values that *a* can take, are Int, Float, Double or any other data type and we call that Maybe is parametrized over type *a*. So what is the type of *a *? In Haskell, we call it Kind[1]. A kind system is essentially a simply typed lambda calculus “one level up”, endowed with a primitive type, denoted * and called “type”, which is the kind of any data type which does not need any type parameters.

λ> :k Int Int :: * λ> :k Float Float :: * λ> :k (*) λ> :k Maybe Maybe :: * -> * λ> :k (Maybe Int) (Maybe Int) :: *

If we change the condition that rather that substituting types (Int, Float, Double, Maybe Int) for *a*, we can substitute it for values like 3, 4 so hypothetically you can think of type of Just 3 as Maybe 3 and not Maybe Int. The hello world program (List with length) of dependent type follow the same intuition.

*HHDL *Data/Vect> :t Vect Data.VectType.Vect.Vect : Nat -> Type -> Type *HHDL *Data/Vect> :doc Vect Data type Vect : Nat -> Type -> Type Constructors: Nil : Vect 0 a (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a

Vector is data type takes a natural number (0, 1, 2 …) and type (Int, Float, Double and many more). We can see that on contrary to Haskell, now values are appearing in types. It has two constructor Nil and Cons (::). Nil is vector of length 0 and polymorphic over* a*. Cons (::) take an element of type *a* and vector of length n and gives a vector of length of (n + 1). We have computation at the time of type checking and what makes type-checking dependently-typed programs difficult is the problem of type equality. Since expressions can appear in types, deciding whether two types are equal requires deciding whether program expressions are equal. This is quite difficult, and if the programming language permits an unrestricted general recursion operator then it becomes undecidable. If you confine non-termination and other side-effects to a monad or the like, then type-checking can remain decidable [2]. To put it simply, what would happen if we have a expression like this appears at type level? It will not terminate!

nonterm :: a nonterm = nonterm

What we can do with dependent types. We can write more precise code and reason about their correctness. Here Tyfun is type level function that takes Boolean value and returns a Type. If the value is False then it returns a function type from Nat to Nat and otherwise a function type which takes two natural numbers (Nat) and returns Bool. The boolornat function takes a boolean value and returns the corresponding value level function.

Tyfun : Bool -> Type Tyfun False = Nat -> Nat Tyfun True = Nat -> Nat -> Bool boolornat : ( b : Bool ) -> Tyfun b boolornat False = \e => e + 1 boolornat True = \x => \y => x == y *Matrix> boolornat True 3 4 False : Bool Metavariables: Main.addField *Matrix> boolornat True 3 3 True : Bool Metavariables: Main.addField *Matrix> boolornat False 3 4 : Nat

We can capture the properties of matrix multiplication like multiplying two matrices of size M x N and N x P will give matrix of size M x P.

transposeMat : {a : Type} -> {m : Nat} -> {n : Nat} -> Vect m (Vect n a) -> Vect n (Vect m a) transposeMat {n = Z} _ = [] --[[],[],[],[].... all the inner vector will have length 0 ] transposeMat {n = S m'} xs = map head xs :: transposeMat (map tail xs) dotP : (Num a) => {m : Nat} -> Vect m a -> Vect m a -> a dotP xs ys = sum (zipWith (*) xs ys) matMult : (Num a) => Vect m (Vect n a) -> Vect p (Vect n a) -> Vect m (Vect p a) matMult {m = Z} _ _ = [] matMult {m = S m'} (x :: xs) ys = map (dotP x) ys :: matMult xs ys matrixMult : (Num a) => Vect m (Vect n a) -> Vect n (Vect p a) -> Vect m (Vect p a) matrixMult xs ys = matMult xs (transposeMat ys) matrixAdd : (Num a) => {m : Nat} -> {n : Nat} -> Vect m (Vect n a) -> Vect m (Vect n a) -> Vect m (Vect n a) matrixAdd {m = Z} {n} _ _ = [] matrixAdd {m = S m} {n} (x :: xs) (y :: ys) = zipWith (+) x y :: matrixAdd {m} {n} xs ys *Matrix> matrixAdd [[1,2,3]] [[1,2,3]] [[2, 4, 6]] : Vect 1 (Vect 3 Integer) Metavariables: Main.addField *Matrix> matrixAdd [[1,2,3]] [[1,2,3],[1,2,3]] (input):1:22:When elaborating argument xs to constructor Data.VectType.Vect.::: Can't unify Vect (S n) a1 (Type of x :: xs) with Vect 0 (Vect 3 a) (Expected type) Specifically: Can't unify S n with 0

For me using the dependent types in program is highly creative aspect and I still find this hard to use but it’s fun. Some resources which I have found very useful for learning. Idris [3], Coq [4], Dependent types at work [5], Type Theory Foundation [6] [7]. I am not expert in dependent type programming so if you have any suggestion/feedback then please drop your comment.

[1] http://en.wikipedia.org/wiki/Kind_%28type_theory%29

[2] http://lambda-the-ultimate.org/node/1129#comment-12313

[3] http://docs.idris-lang.org/en/latest/

[4] https://coq.inria.fr/

[5] http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf

[6] https://www.youtube.com/watch?v=ev7AYsLljxk

[7] http://okmij.org/ftp/Haskell/dependent-types.html

## Computing a^n using binary representation of natural number in Agda

While following the Agda tutorial, I wrote this code to compute a^{n}. Not very elegant example probably because I am not expert and still learning about dependent types. Maybe after getting some more experience and knowledge, I will try to prove the correctness and complexity of this algorithm. See the post of Twan van Laarhoven about proving correctness and complexity of merge sort in Agda.

module PowerFunction where data ℕ⁺ : Set where one : ℕ⁺ double : ℕ⁺ → ℕ⁺ double⁺¹ : ℕ⁺ → ℕ⁺ add : ℕ⁺ → ℕ⁺ → ℕ⁺ add one one = double one add one ( double x ) = double⁺¹ x add one ( double⁺¹ x ) = double ( add x one ) add ( double x ) one = double⁺¹ x add ( double x ) ( double y ) = double ( add x y ) add ( double x ) ( double⁺¹ y ) = double⁺¹ ( add x y ) add ( double⁺¹ x ) one = double ( add x one ) add ( double⁺¹ x ) ( double y ) = double⁺¹ ( add x y ) add ( double⁺¹ x ) ( double⁺¹ y ) = double ( add ( add x y ) one ) mult : ℕ⁺ → ℕ⁺ → ℕ⁺ mult x one = x mult x ( double y ) = double ( mult x y ) mult x ( double⁺¹ y ) = add x ( double ( mult x y ) ) pow : ℕ⁺ → ℕ⁺ → ℕ⁺ pow one _ = one pow x one = x pow x ( double one ) = mult x x pow x ( double y ) = pow ( pow x y ) ( double one ) pow x ( double⁺¹ y ) = mult x ( pow ( pow x y ) ( double one ) )

Computing 2 ^ 6

pow ( double one ) ( double ( double⁺¹ one ))

double (double (double (double (double (double one)))))

If you have suggestion then please let me know.