Short Introduction to Dependently Typed Programing in Idris given at FATA Seminars 22/23

FATA.idr

||| #+TITLE: Dependently Typed Functional Programming
||| #+AUTHOR: Jan de Muijnck-Hughes
||| #+DATE: FATA Seminar 22/23
||| #+STARTUP: noindent overview

module FATA

%default total

-- # Abstract

{-

Dependent Type Systems [1,2] allow types to depended on values. When combined with Functional Programming [3], we get an expressive environment in which to reason with and about our programs. This arises from the Curry-Howard Correspondence [4] in which: "Propositions are Types; Proofs are Programs".

Idris2 is a general purpose functional language [5] with dependent & quantitative types (how & when terms are used [6]), and is a wonderful tool in which to not only perform mechanised reasoning about programs, but to run them too.

In this little tutorial, we will look at how we can use Idris2 to reason about, and perform, two of the most _fundamental problems_ in programming:

1. adding two numbers together; and
2. appending lists.

Thus demonstrating key aspects of how Idris2 is used for theory and in practice.

I am hoping that at the end of the 30-ish minutes, you will get an itch to see how dependent-types can help you with your work.

Please ask questions through out!

[1] https://en.wikipedia.org/wiki/Dependently_typed_programming
[2] https://en.wikipedia.org/wiki/Intuitionistic_type_theory
[3] https://en.wikipedia.org/wiki/Functional_programming
[4] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
[5] https://www.idris-lang.org
[6] https://en.wikipedia.org/wiki/Substructural_type_system

-}

-- # Objectives

{-

Introduction to Dependently-Typed Functional Programming by example.

We will be using Idris <https://www.idris-lang.org>

Two objectives:

1. How to add two natural numbers.
2. How to append two lists.

-}

-- # Representing Numbers

-- ## Definition

{-

Peano numbers are a simple model to reason about arithmetic of
Natural/Whole numbers.

-}

data Peano = Zero      -- There is nothing, the base case;
                       -- or
           | Inc Peano -- there is one more.

%name Peano i, j, k

Natural : Type
Natural = Peano

Whole : Type
Whole = Natural


-- ## Examples

{-

We also introduce interactive editing:

-}

zero : Natural

one : Whole

two : Peano


-- # How hard is it to add peano's together?

-- ## A (Dis)Functional Implementation

plus : (a,b : Peano) -> Peano

-- ### Question:

{-

Is the definition of =plus= correct?

Let's test it to find out?

-}

-- ### A Functional Implementation

plus' : (a,b : Peano) -> Peano
plus' Zero b
  = b

plus' (Inc x) b
  = Inc $ plus' x b

{-

We know this definition is correct, but how can we:

1. Verify that it is correct?
2. Have a practical implementation?

-}

-- ### A Correct-By-Construction Implementation

{-

Let us begin by encoding the _correct_ rules for addition.

-}

data Plus : (a,b,c : Peano) -> Type
  where
    ||| Base case.
    |||
    ||| ```
    |||    0 + b = b
    ||| ```
    ZI : Plus Zero b b

    ||| Induction on left operand.
    |||
    ||| ```
    ||| S(a) + b = S(a+b)
    ||| ```
    IA : (step : Plus      x  b      c)
              -> Plus (Inc x) b (Inc c)

-- #### Existential Quantification

{-
A mechanism to evidence the result.

That is we want to state the following:

#+begin_example
Given two natural numbers: a, b.
There exists a number c such that the following holds:

   a + b = c
#+end_example

We do so using a dependent pair:

-}


data SuchThat : (type : Type)
             -> (p    : type -> Type)
                     -> Type
  where
    ST : (val : type)
      -> (prf : p val)
             -> SuchThat type p

-- ##### Note: It is Predefined

{-

Actually predefined in the language as:

-}


foo : (a,b : Peano) -> (c ** Plus a b c)


-- or

foo : (a,b : Peano) -> DPair Peano (Plus a b)

-- ### Back to the 'Proof'.

safePlus : (a,b : Peano)
               -> DPair Peano (Plus a b)

-- ### Checking that: a + b = c

{-

We want to do this:

-}

check : (a,b,c : Peano) -> Plus a b c

{-

This will not hold for all inputs.

-}

-- ### Intermezzo: Decidable.

data Holds : (pred : type) -> Type where
  Yes : (prf : pred) -> Holds pred
  No  : (prf : pred -> Void) -> Holds pred

-- This is =Dec= within Idris.

-- ### Back to Checking

-- #### Some helpers to state impossible cases.

Uninhabited (Plus Zero (Inc x) Zero) where
  uninhabited ZI impossible

Uninhabited (Plus Zero Zero (Inc x)) where
  uninhabited ZI impossible

Uninhabited (Plus (Inc x) b Zero) where
  uninhabited ZI impossible

-- #### The Implementation

plusCheck : (a,b,c : Peano) -> Dec (Plus a b c)

-- ### Linking Verified Implementations to Non-Verified ones.

-- We can link using /Propositional Equality/.

-- #### The Equality Type

-- It is built in as (=Equal=, =(=)=), but here is a similar definition.

data Same : (a,b : type) -> Type
  where
    EQ : Same a a

||| Bound the implicits to show LHS magic.
transitive : {a,b,c : Peano}
          -> Same a b
          -> Same   b c
          -> Same a   c

-- ### Link things using a Lemma

plusSame : (prf : Plus  a b   c)
               -> plus' a b = c

-- # How hard is it to add two lists together?

-- ## A (Dis)Functional Implementation

data List' a = Empty
             | Extend a (List' a)

xs,ys : List' Nat

xs = Extend 1 (Extend 2 (Extend 3 Empty))
ys = Extend 6 (Extend 7 (Extend 8 Empty))

listAppend : (xs,ys : List' a) -> List' a


-- ## Do we need to prove everything?

{-

Could go through and define =ListAppend=, and write those predicates.

Notice the structure of =List'= and =Peano=: /Nothing; or one more/.

-}

-- ## Lists with Length!

namespace Vect
  public export
  data Vect : (count : Peano)
           -> (type  : Type)
                    -> Type
    where
      Empty : Vect Zero type
      Extend : (value : type)
            -> (rest  : Vect      c  type)
                     -> Vect (Inc c) type

vs,ws : Vect (Inc (Inc (Inc Zero))) Nat

vs = Extend 1 (Extend 2 (Extend 3 Empty))
ws = Extend 6 (Extend 7 (Extend 8 Empty))

-- ## Implementing Append

append : (xs : Vect       a    type)
      -> (ys : Vect         b  type)
            -> Vect (plus a b) type

-- ##Is this correct?

{-

*No*, our implementation is guided by a bad specification.

How do we correct this mistake?

-}

-- ## A Guided Implementation of List Append.

-- Let us use the /correct/ implementation!

-- [ Note ] If running out of time: C-c C-g

append' : (xs : Vect        a    type)
       -> (ys : Vect          b  type)
             -> Vect (plus' a b) type

-- # Conclusion:

{-
+ Types keep you honest!

+ Shown fundamental building blocks in using languages like Idris.

  + Other Systems: Lean, Agda, & Coq

+ Mechanised Formal Methods

  + Curry-Howard Correspondence in action.
  + Scalable:
    + Verified Peano Arithmetic.
    + Verified implementations of STLC.
    + Verified implementations of (Middleweight)Java.
  + Trade-Offs in how much we verify & when.

+ Recommended Reading

  + Programming Language Foundations in Agda
  + Software Foundations (Coq)
  + Type-Driven Development in Idris

+ Not covered

  + Quantified Reasoning on variable usage...
  + View-Patterns...
  + Other Design Patterns...
  + ...

-}

-- [ EOF ]

FATALive.org

Dependently Typed Functional Programming

module FATALive

%default total

Can those at the back read this sentence?

Abstract

Dependent Type Systems [1,2] allow types to depended on values. When combined with Functional Programming [3], we get an expressive environment in which to reason with and about our programs. This arises from the Curry-Howard Correspondence [4] in which: “Propositions are Types; Proofs are Programs”.

Idris2 is a general purpose functional language [5] with dependent & quantitative types (how & when terms are used [6]), and is a wonderful tool in which to not only perform mechanised reasoning about programs, but to run them too.

In this little tutorial, we will look at how we can use Idris2 to reason about, and perform, two of the most fundamental problems in programming:

1. adding two numbers together; and
2. appending lists.

Thus demonstrating key aspects of how Idris2 is used for theory and in practice.

I am hoping that at the end of the 30-ish minutes, you will get an itch to see how dependent-types can help you with your work.

Please ask questions through out!

[1] https://en.wikipedia.org/wiki/Dependently_typed_programming [2] https://en.wikipedia.org/wiki/Intuitionistic_type_theory [3] https://en.wikipedia.org/wiki/Functional_programming [4] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence [5] https://www.idris-lang.org [6] https://en.wikipedia.org/wiki/Substructural_type_system

Objectives

Introduction to Dependently-Typed Functional Programming by example.

We will be using Idris https://www.idris-lang.org

Two objectives:

1. How to add two natural numbers.
2. How to append two lists.

Representing Numbers

Definition

Peano numbers are a simple model to reason about arithmetic of Natural/Whole numbers.

data Peano = Zero      -- There is nothing, the base case;
                       -- or
           | Inc Peano -- there is one more.

%name Peano i, j, k

Natural : Type
Natural = Peano

Whole : Type
Whole = Natural

Examples

We also introduce interactive editing:

zero : Natural

one : Whole

two : Peano

How hard is it to add peano’s together?

A (Dis)Functional Implementation

plus : (a,b : Peano) -> Peano

Question:

Is the definition of plus correct?

Let’s test it to find out?

A Functional Implementation

plus' : (a,b : Peano) -> Peano
plus' Zero b
  = b

plus' (Inc x) b
  = Inc $ plus' x b

We know this definition is correct, but how can we:

1. Verify that it is correct?
2. Have a practical implementation?

A Correct-By-Construction Implementation

Let us begin by encoding the correct rules for addition.

data Plus : (a,b,c : Peano) -> Type
  where
    ||| Base case.
    |||
    ||| ```
    |||    0 + b = b
    ||| ```
    ZI : Plus Zero b b

    ||| Induction on left operand.
    |||
    ||| ```
    ||| S(a) + b = S(a+b)
    ||| ```
    IA : (step : Plus      x  b      c)
              -> Plus (Inc x) b (Inc c)

Intermezzo: Existential Quantification

A mechanism to evidence the result.

That is we want to state the following:

Given two natural numbers: a, b.
There exists a number c such that the following holds:

   a + b = c

We do so using a dependent pair:

data SuchThat : (type : Type)
             -> (p    : type -> Type)
                     -> Type
  where
    ST : (val : type)
      -> (prf : p val)
             -> SuchThat type p

Note: It is Predefined

Actually predefined in the language as:

foo : (a,b : Peano) -> (c ** Plus a b c)

or

foo : (a,b : Peano) -> DPair Peano (Plus a b)

Back to the ‘Proof’.

safePlus : (a,b : Peano)
               -> DPair Peano (Plus a b)

Checking that: a + b = c

We want to do this:

check : (a,b,c : Peano) -> Plus a b c

This will not hold for all inputs.

Intermezzo: Decidable.

data Holds : (pred : type) -> Type where
  Yes : (prf : pred) -> Holds pred
  No  : (prf : pred -> Void) -> Holds pred

This is Dec within Idris.

Back to Checking

Some helpers to state impossible cases.

Uninhabited (Plus Zero (Inc x) Zero) where
  uninhabited ZI impossible

Uninhabited (Plus Zero Zero (Inc x)) where
  uninhabited ZI impossible

Uninhabited (Plus (Inc x) b Zero) where
  uninhabited ZI impossible

The Implementation

plusCheck : (a,b,c : Peano) -> Dec (Plus a b c)

Linking Verified Implementations to Non-Verified ones.

We can link using Propositional Equality.

The Equality Type

It is built in as (Equal, ()=), but here is a similar definition.

data Same : (a,b : type) -> Type
  where
    EQ : Same a a

||| Bound the implicits to show LHS magic.
transitive : {a,b,c : Peano}
          -> Same a b
          -> Same   b c
          -> Same a   c

Link things using a Lemma

plusSame : (prf : Plus  a b   c)
               -> plus' a b = c

How hard is it to add two lists together?

A (Dis)Functional Implementation

data List' a = Empty
             | Extend a (List' a)

xs,ys : List' Nat

xs = Extend 1 (Extend 2 (Extend 3 Empty))
ys = Extend 6 (Extend 7 (Extend 8 Empty))

listAppend : (xs,ys : List' a) -> List' a

Do we need to prove everything?

Could go through and define ListAppend, and write those predicates.

Notice the structure of List' and Peano: Nothing; or one more.

Lists with Length!

namespace Vect
  public export
  data Vect : (count : Peano)
           -> (type  : Type)
                    -> Type
    where
      Empty : Vect Zero type
      Extend : (value : type)
            -> (rest  : Vect      c  type)
                     -> Vect (Inc c) type

vs,ws : Vect (Inc (Inc (Inc Zero))) Nat

vs = Extend 1 (Extend 2 (Extend 3 Empty))
ws = Extend 6 (Extend 7 (Extend 8 Empty))

Implementing Append

append : (xs : Vect       a    type)
      -> (ys : Vect         b  type)
            -> Vect (plus a b) type

Is this correct?

No, our implementation is guided by a bad specification.

How do we correct this mistake?

A Guided Implementation of List Append.

Let us use the correct implementation!

-- [ Note ] If running out of time: C-c C-g

append' : (xs : Vect        a    type)
       -> (ys : Vect          b  type)
             -> Vect (plus' a b) type

Conclusion:

Types keep you honest!

Shown fundamental building blocks in using languages like Idris.

• Other Systems: Lean, Agda, & Coq

Mechanised Formal Methods

• Curry-Howard Correspondence in action.
• Scalable:
  • Verified Peano Arithmetic.
  • Verified implementations of STLC.
  • Verified implementations of (Middleweight)Java.
• Trade-Offs in how much we verify & when.

Recommended Reading

• Programming Language Foundations in Agda
• Software Foundations (Coq)
• Type-Driven Development in Idris

Not covered

• Quantified Reasoning on variable usage…
• View-Patterns…
• Other Design Patterns…
• …