Dependent Type Playground for SoCraTes CH 2023

Session_1.idr

-- https://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#dependent-types
import Data.Vect
    
insertionSort : (Ord a) => Vect n a -> Vect n a
insertionSort [] = []
insertionSort (x::xs) = insert x (insertionSort xs) where
    insert : (Ord a) => a -> Vect n a -> Vect (S n) a
    insert v [] = [v]
    insert v (l::ls) = if v <= l then v :: l :: ls else l :: (insert v ls)
        
        
repeat : (n : Nat) -> a -> Vect n a
repeat Z _ = []
repeat (S k) v = v :: repeat k v

 -- example for pattern match
data Shape = Circle Double | Square Double

calc : Shape -> Double
calc (Circle r) = r
calc (Square l) = l



data Player = X | O

data Game : Player -> Type where
    G : (p : Player) -> Game p


nextPlayer : (p : Player) -> Player
nextPlayer X = O
nextPlayer O = X

play : (p : Player) -> Game p -> Game (nextPlayer p)
play O (G O) = (G X)
play X (G X) = (G O)

Session_2.idr

import Data.Vect

{-
  1. Type Driven Development with Idris by Edwin Brady
  2. Type - Define - Redefine
  4. The Compiler as your Pairing Partner
  3. Example 1: Add Vectors
  4. Example 2: Insertion Sort
  5. Discussion?
-}

-- add two vectors of same length
addVector : (Num a) => Vect n a -> Vect n a -> Vect n a
addVector [] [] = []
addVector (x :: xs) (y :: ys) = x + y :: addVector xs ys

total
insert : Ord a => a -> Vect len a -> Vect (S len) a
insert v [] = [v]
insert v (smallest :: rest) = if v <= smallest
  then v :: smallest :: rest
  else smallest :: (insert v rest)

-- insertion sort
total
insSort : (Ord a) => Vect n a -> Vect n a
insSort [] = []
insSort (first :: rest) = insert first (insSort rest)

-- custom implementation of natural numbers
data N = Zero | Succ N

-- add two natural numbers
plus : N -> N -> N
plus Zero y = y
plus (Succ x) y = Succ (plus x y)

-- proof that plus reduces on the left side
zeroReducesL : (n : N) -> plus Zero n = n
zeroReducesL v = ?rest

-- proof that plus reduces on the right side
zeroReducesR : (n : N) -> plus n Zero = n
zeroReducesR Zero = Refl
zeroReducesR (Succ x) = rewrite zeroReducesR x in Refl