Maths - Idris code for Dependent Types

Idris Examples

Vectors

In both the dependent sum type and the dependent product type examples below the type declaration has two terms where the second depends on the first. However the definition of the sum type requires a specific value wheras the definition of the product type applies to all possible values.

Dependent Sum Type

(dependent pair)

myvect : (n:Nat ** Vect n String)
myvect = (3 ** ("a", "b", "c")
Dependent Product Type
myvect : n:Nat  -> (Vect n String)
myvect n = 3 *n

Implemetations of Dependent Product Type

Vect is an example of a type which depends on:

  • Another type 'elem'
  • A Nat number 'len' - this makes it a dependent type.
||| Vectors: Generic lists with explicit length in the type
||| @ len the length of the list
||| @ elem the type of elements
data Vect : (len : Nat) -> (elem : Type) -> Type where
  ||| Empty vector
  Nil  : Vect Z elem
  ||| A non-empty vector of length `S len`, consisting of
  ||| a head element and the rest of the list, of length `len`.
  (::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem

So in this example we are saying that Vect exists for all types 'elem' and for all numbers 'len'.

Most programs that support this have a special notation for it.

So this is a product type where one of the types is a function (family of types).

So instead of the usual product:   Pair A B
we have :   DPair A (A -> Type)
For example:   DPair Nat (Nat -> Type)
There is a special notation in Idris:   A ** (A -> Type)

Notation

dependent sum notation
~> idris -p base Data/Vect.idr
 
    /  _/___/ /____(_)____ 
    / // __  / ___/ / ___/     Version 1.3.2
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/ 
 /___/\__,_/_/  /_/____/       Type :? for help

Idris is free software with ABSOLUTELY NO WARRANTY. 
For details type :warranty.
*Data/Vect> (n : Nat ** Vect n String)
(n : Nat ** Vect n String) : Type
  

Example

In the introduction dependent types were introduced with the example of vect.

specificVect : (n : Nat ** Vect n String)
specificVect = (3 ** ["a","b","c"])
  
We can also show dependent sum types using Vect.
*typeTheory> specificVect
(3 ** ["a", "b", "c"]) : (n : Nat ** Vect n String)
  

In the product case there was a type for every n which is represented by a function (n -> Vect n elem). In the sum case there is one type given by a single 'n' which is represented by a product/tuple (n ** Vect n elem) but because the second element of the tuple depends on the first '**' is used to seperate the elements instead of ','.

Example - Expressions

The aim here is to try to model the context of variable declarations (or of premises in logic) as an index.

Start by creating a very simple expression type to work with.
||| Expression over some type 't'
data Expression t =
   Lit  t
   Var String
   (+) (Expression t) (Expression t)
Now give it the ability to bind
||| Expression which binds some variable 'v'
data BindExpression t (v:String) =
   BoundVar v (Expression t)
   Nested v (BindExpression t v)

I haven't yet worked this through.

Example - Variable Scope

Here we try to model the situation where we define variables and then use them either in the same block or in a sub block. So we need to determine which definition to use based on the scope.

How can we revers the arrows so that we can get back to a definition from a variable use?

  variable scope
   

 

Implementation Code

dependent pair

Idris

from : Idris-dev/libs/prelude/Builtins.idr

  ||| Dependent pairs aid in the construction of dependent types by
  ||| providing evidence that some value resides in the type.
  |||
  ||| Formally, speaking, dependent pairs represent existential
  ||| quantification - they consist of a witness for the existential
  ||| claim and a proof that the property holds for it.
  |||
  |||  @a the value to place in the type.
  |||  @P the dependent type that requires the value.
  data DPair : (a : Type) -> (P : a -> Type) -> Type where
      MkDPair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> DPair a P
  

Dependent Types in Programming

In the language 'Scala' we can define a type that is parameterised by another type (polymorphism) for instance:
List[T]

This represents a list of any type, represented by 'T', for example a list of Integers or a list of boolean values.

However, Scala does not allow dependent products like say: Modulo[n:Integer] which would represent any modulo number system such as modulo 3 or modulo 27.


metadata block
see also:
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flag Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.

 

Terminology and Notation

Specific to this page here:

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.