My Weblog

Blog about programming and math

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

May 15, 2015 Posted by | Idris, Programming | , , | Leave a comment

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

While following the Agda tutorial, I wrote this code to compute an. 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.

June 12, 2013 Posted by | Agda, Programming | , , , | 2 Comments