add 8/99 haskell problems and some of hottest-2022
This commit is contained in:
parent
71c95c351e
commit
081f13ab50
|
@ -0,0 +1,24 @@
|
||||||
|
open import general-notation
|
||||||
|
|
||||||
|
data Bool : Type where
|
||||||
|
true : Bool
|
||||||
|
false : Bool
|
||||||
|
|
||||||
|
-- non-dependently typed if-then-else
|
||||||
|
if_then_else : {A : Type} → Bool → A → A → A
|
||||||
|
if true then x else y = x
|
||||||
|
if false then x else y = y
|
||||||
|
|
||||||
|
|
||||||
|
_&&_ : Bool → Bool → Bool
|
||||||
|
true && true = true
|
||||||
|
x && y = false
|
||||||
|
|
||||||
|
_||_ : Bool → Bool → Bool
|
||||||
|
false || false = false
|
||||||
|
x || y = true
|
||||||
|
|
||||||
|
infix 20 _||_
|
||||||
|
infix 30 _&&_
|
||||||
|
-- higher precedence level, higher the number, I guess.
|
||||||
|
|
|
@ -0,0 +1,9 @@
|
||||||
|
open import general-notation
|
||||||
|
|
||||||
|
data List (A : Type) : Type where
|
||||||
|
[] : List A
|
||||||
|
_::_ : A → List A → List A
|
||||||
|
|
||||||
|
infixr 10 _::_
|
||||||
|
|
||||||
|
List-elim : {A : (X : Type)
|
|
@ -0,0 +1,9 @@
|
||||||
|
- Agda: Martin Escardo - 1: [[file:./lecture1.agda]]
|
||||||
|
+ [X] Pre-made: [[file:./general-notation.agda]]
|
||||||
|
+ [ ] Pre-made: [[file:./sums.agda]]
|
||||||
|
+ [ ] Pre-made: [[file:./empty-type.agda]]
|
||||||
|
+ [ ] Pre-made: [[file:./Bool.agda]]
|
||||||
|
+ [ ] Pre-made: [[file:./Vector.agda]]
|
||||||
|
+ [ ] Pre-made: [[file:./natural-numbers-type.agda]]
|
||||||
|
+ [ ] Pre-made: [[file:./natural-numbers-functions.agda]]
|
||||||
|
+ [ ] Pre-made: [[file:./unit-type.agda]]
|
|
@ -0,0 +1,13 @@
|
||||||
|
open import general-notation
|
||||||
|
open import natural-numbers-type
|
||||||
|
|
||||||
|
data Vector (A : Type) : ℕ → Type where
|
||||||
|
[] : Vector A 0
|
||||||
|
_::_ : {n : ℕ} → Vector A n → Vector A (suc n)
|
||||||
|
|
||||||
|
infixr 10 _::_
|
||||||
|
|
||||||
|
-- Vector-elim {X : Type}
|
||||||
|
-- → {A : (n : ℕ) → Vector X n → Type}
|
||||||
|
-- → A 0 []
|
||||||
|
-- → (k : ℕ) (vk : Vector X k) (vk' : Vector X (suc k)) → A k vk → A (S k) vk'
|
|
@ -0,0 +1,21 @@
|
||||||
|
open import general-notation
|
||||||
|
|
||||||
|
-- Empty type means no constructors.
|
||||||
|
-- It is impossible build a value of type 𝟘.
|
||||||
|
-- Coq analogue could be False type.
|
||||||
|
data 𝟘 : Type where
|
||||||
|
|
||||||
|
|
||||||
|
¬_ : Type → Type
|
||||||
|
¬ A = A → 𝟘
|
||||||
|
|
||||||
|
infix 1000 ¬_
|
||||||
|
|
||||||
|
-- Elimination principle
|
||||||
|
-- Propery A holds for all values of type 𝟘
|
||||||
|
-- kinda like forall x:𝟘, A x in coq
|
||||||
|
𝟘-elim : {A : 𝟘 → Type} (x : 𝟘) → A x
|
||||||
|
𝟘-elim ()
|
||||||
|
-- no pattern. An empty list of equations
|
||||||
|
-- vacuous truth
|
||||||
|
|
|
@ -0,0 +1,30 @@
|
||||||
|
{-# OPTIONS --without-K --allow-unsolved-metas #-}
|
||||||
|
|
||||||
|
module exercise-2022-07-06 where
|
||||||
|
|
||||||
|
open import lecture1
|
||||||
|
-- open import prelude hiding (not-is-involution)
|
||||||
|
|
||||||
|
-- _&&'_ : Bool → Bool → Bool
|
||||||
|
-- a &&' b = ?
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
_&&'_ : Bool → Bool → Bool
|
||||||
|
true &&' true = true
|
||||||
|
true &&' false = false
|
||||||
|
false &&' true = false
|
||||||
|
false &&' false = false
|
||||||
|
|
||||||
|
_xor_ : Bool → Bool → Bool
|
||||||
|
true xor true = false
|
||||||
|
true xor false = true
|
||||||
|
false xor true = true
|
||||||
|
false xor false = false
|
||||||
|
|
||||||
|
--_^_ : ℕ → ℕ → ℕ
|
||||||
|
--a ^ zero = 1
|
||||||
|
--a ^ suc b = {!(a ^ b) * a!}
|
||||||
|
|
||||||
|
-- _! : ℕ → ℕ
|
|
@ -0,0 +1,29 @@
|
||||||
|
{-# OPTIONS --without-K --safe #-}
|
||||||
|
-- safe disables experimental agda features
|
||||||
|
|
||||||
|
module general-notation where
|
||||||
|
|
||||||
|
-- Type are called an Sets in agda.
|
||||||
|
-- Because in HoTT, only /some/ type are called Sets.
|
||||||
|
-- And there are type which are not sets.
|
||||||
|
-- Making an alias
|
||||||
|
Type = Set
|
||||||
|
Type₁ = Set₁
|
||||||
|
|
||||||
|
-- Find type of a value
|
||||||
|
type-of : {X : Type} → X → Type
|
||||||
|
type-of {X} x = X
|
||||||
|
|
||||||
|
-- Find domain of a function
|
||||||
|
domain : {X Y : Type} → (X → Y) → Type
|
||||||
|
domain {X} {Y} f = X
|
||||||
|
|
||||||
|
-- Find codomain of a function
|
||||||
|
codomain : {X Y : Type} → (X → Y) → Type
|
||||||
|
codomain {X} {Y} f = Y
|
||||||
|
|
||||||
|
-- A notation to avoid too many parenthesis
|
||||||
|
_$_ : {X Y : Type} → (X → Y) → X → Y
|
||||||
|
f $ g = f g
|
||||||
|
|
||||||
|
infix 0 _$_
|
|
@ -0,0 +1,151 @@
|
||||||
|
{-# OPTIONS --without-K --safe #-}
|
||||||
|
-- safe disables experimental agda features
|
||||||
|
-- without-K: related to HoTT. equality, identity, etc or something like that.
|
||||||
|
-- by default agda is inconsistant with HoTT. To get around that.
|
||||||
|
|
||||||
|
open import general-notation
|
||||||
|
|
||||||
|
data Bool : Type where
|
||||||
|
true : Bool
|
||||||
|
false : Bool
|
||||||
|
|
||||||
|
not : Bool → Bool
|
||||||
|
not true = false
|
||||||
|
not false = true
|
||||||
|
|
||||||
|
not' : Bool → Bool
|
||||||
|
-- not b = ?
|
||||||
|
-- not' b = { }0
|
||||||
|
--
|
||||||
|
-- C-c C-, (couldn't make it work)
|
||||||
|
--
|
||||||
|
-- C-c C-c
|
||||||
|
-- not' true = { }0
|
||||||
|
-- not' false = { }1
|
||||||
|
--
|
||||||
|
-- Fill in false and C-c C-SPC
|
||||||
|
not' true = false
|
||||||
|
not' false = true
|
||||||
|
|
||||||
|
|
||||||
|
idBool : Bool → Bool
|
||||||
|
idBool b = b
|
||||||
|
-- or
|
||||||
|
|
||||||
|
idBool' : Bool → Bool
|
||||||
|
idBool' = λ x → x
|
||||||
|
|
||||||
|
idBool'' : Bool → Bool
|
||||||
|
-- idBool'' = λ (x : ?) → x
|
||||||
|
-- and do C-c C-s
|
||||||
|
idBool'' = λ (x : Bool) → x
|
||||||
|
|
||||||
|
-- A Pi type
|
||||||
|
id : {X : Type} → X → X
|
||||||
|
id x = x
|
||||||
|
|
||||||
|
|
||||||
|
idBool3 : Bool → Bool
|
||||||
|
-- idBool'' = λ (x : ?) → x
|
||||||
|
-- and do C-c C-s
|
||||||
|
idBool3 = id {Bool} -- Explicit parameter
|
||||||
|
--
|
||||||
|
-- or
|
||||||
|
-- idBool3 = id -- Implicit parameter. Possible when there is only a unique value possible and agda can figure it out
|
||||||
|
--
|
||||||
|
-- or
|
||||||
|
-- idBool3 = id _ -- Asking agda to figure it out.
|
||||||
|
|
||||||
|
|
||||||
|
-- | Propositions as types
|
||||||
|
example : {P Q : Type} → P → (Q → P)
|
||||||
|
example {P} {Q} p = f
|
||||||
|
where
|
||||||
|
f : Q → P
|
||||||
|
f q = p
|
||||||
|
-- or
|
||||||
|
-- f _ = p -- here, the underscore means something like a 'don't care'
|
||||||
|
|
||||||
|
example' : {P Q : Type} → P → (Q → P)
|
||||||
|
-- example' {P} {Q} p = {λ q → ? }0
|
||||||
|
example' {P} {Q} p = λ (q : Q) → p
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
-- | Natural numbers
|
||||||
|
data ℕ : Type where
|
||||||
|
zero : ℕ
|
||||||
|
suc : ℕ → ℕ
|
||||||
|
|
||||||
|
three : ℕ
|
||||||
|
three = suc (suc (suc zero))
|
||||||
|
|
||||||
|
{-# BUILTIN NATURAL ℕ #-}
|
||||||
|
-- Can use normal numbers to associate it with
|
||||||
|
-- the ℕ that we just defined
|
||||||
|
|
||||||
|
three' : ℕ
|
||||||
|
three' = 3
|
||||||
|
|
||||||
|
D : Bool → Type
|
||||||
|
D true = ℕ
|
||||||
|
D false = Bool
|
||||||
|
|
||||||
|
-- | mix-fix operator
|
||||||
|
-- A use of '_'
|
||||||
|
if_then_else_ : {X : Type} → Bool → X → X → X
|
||||||
|
if true then x else y = x
|
||||||
|
if false then x else y = y
|
||||||
|
|
||||||
|
-- 'if' via a dependent type
|
||||||
|
if[_]_then_else_ : (X : Bool → Type)
|
||||||
|
→ (b : Bool)
|
||||||
|
→ X true
|
||||||
|
→ X false
|
||||||
|
→ X b
|
||||||
|
if[ X ] true then x else y = x
|
||||||
|
if[ X ] false then x else y = y
|
||||||
|
|
||||||
|
|
||||||
|
-- Doubt: Are pi-types same as dependent types?
|
||||||
|
unfamiliar : (b : Bool) → D b
|
||||||
|
unfamiliar b = if[ D ] b then 3 else false
|
||||||
|
-- the branches are of different type!
|
||||||
|
-- Thanks to D being dependently typed.
|
||||||
|
|
||||||
|
data List (A : Type) : Type where
|
||||||
|
[] : List A
|
||||||
|
_::_ : A → List A → List A
|
||||||
|
|
||||||
|
-- right associative with precedence 10
|
||||||
|
-- Can make it left associative by using just 'infix' instead of the 'infixr'
|
||||||
|
infixr 10 _::_
|
||||||
|
|
||||||
|
|
||||||
|
-- 'List' has type 'Type → Type'
|
||||||
|
ff : Type → Type
|
||||||
|
ff = List
|
||||||
|
|
||||||
|
sample-list₀ : List ℕ
|
||||||
|
sample-list₀ = 0 :: 1 :: 2 :: []
|
||||||
|
-- Same as: sample-list₀ = 0 :: (1 :: (2 :: []))
|
||||||
|
|
||||||
|
length : {X : Type} → List X → ℕ
|
||||||
|
length [] = zero
|
||||||
|
length (x :: xs) = suc (length xs)
|
||||||
|
|
||||||
|
|
||||||
|
-- Induction principle for ℕ
|
||||||
|
ℕ-elim : {A : ℕ → Type}
|
||||||
|
→ A 0 -- Base case: We know that A holds for 0
|
||||||
|
→ ((k : ℕ) → A k → A (suc k)) -- Induction step: If A k holds for any natural number k, then A (k+1) holds as well
|
||||||
|
→ (n : ℕ) → A n -- Conclusion: 'A n' hold for any natural number 'n'
|
||||||
|
ℕ-elim {A} a₀ f = h
|
||||||
|
where
|
||||||
|
h : (n : ℕ) → A n
|
||||||
|
h zero = a₀
|
||||||
|
h (suc n) = f n IH
|
||||||
|
where
|
||||||
|
IH : A n -- Induction hypothesis. A recursive call with a smaller n
|
||||||
|
IH = h n
|
||||||
|
|
|
@ -0,0 +1,6 @@
|
||||||
|
open import general-notation
|
||||||
|
open import natural-numbers-type
|
||||||
|
|
||||||
|
max : ℕ → ℕ → ℕ
|
||||||
|
max zero b = b
|
||||||
|
max (suc a) b = {!!}
|
|
@ -0,0 +1,33 @@
|
||||||
|
open import general-notation
|
||||||
|
|
||||||
|
data ℕ : Type where
|
||||||
|
zero : ℕ
|
||||||
|
suc : ℕ → ℕ
|
||||||
|
|
||||||
|
{-# BUILTIN NATURAL ℕ #-}
|
||||||
|
|
||||||
|
-- Doubt: Type formers are same as constructors?
|
||||||
|
ℕ-elim :
|
||||||
|
{A : ℕ → Type}
|
||||||
|
→ A 0
|
||||||
|
→ ((k : ℕ) → A k → A (suc k))
|
||||||
|
→ (n : ℕ) → A n
|
||||||
|
ℕ-elim {A} a₀ f = h
|
||||||
|
where
|
||||||
|
h : (n : ℕ) → A n
|
||||||
|
h zero = a₀
|
||||||
|
h (suc n) = f n (h n)
|
||||||
|
|
||||||
|
|
||||||
|
-- TODO: ℕ-nondep-elim
|
||||||
|
|
||||||
|
_+_ : ℕ → ℕ → ℕ
|
||||||
|
x + zero = x
|
||||||
|
x + suc y = suc (x + y)
|
||||||
|
|
||||||
|
_*_ : ℕ → ℕ → ℕ
|
||||||
|
x * zero = zero
|
||||||
|
x * suc y = y + (x * y)
|
||||||
|
|
||||||
|
infixr 20 _+_
|
||||||
|
infixr 30 _*_
|
|
@ -0,0 +1,30 @@
|
||||||
|
open import general-notation
|
||||||
|
|
||||||
|
data Σ0 {A : Type} (B : A → Type) : Type where
|
||||||
|
_,_ : (x : A) (y : B x) → Σ0 {A} B
|
||||||
|
|
||||||
|
pr₁0 : {A : Type} {B : A → Type} (z : Σ0 B) → A
|
||||||
|
pr₁0 (x , y) = x
|
||||||
|
|
||||||
|
pr₂0 : {A : Type} {B : A → Type} (z : Σ0 B) → B (pr₁0 z)
|
||||||
|
pr₂0 (x , y) = y
|
||||||
|
|
||||||
|
record Σ {A : Type} (B : A → Type) : Type where
|
||||||
|
constructor
|
||||||
|
_,_
|
||||||
|
field
|
||||||
|
pr₁ : A
|
||||||
|
pr₂ : B pr₁
|
||||||
|
|
||||||
|
open Σ public
|
||||||
|
-- public to make even the module importing this would have Σ
|
||||||
|
|
||||||
|
infix 0 _,_
|
||||||
|
-- default is right associative
|
||||||
|
-- (a, (b, c)) is same as (a, b, c)
|
||||||
|
|
||||||
|
Sigma : (A : Type) (B : A → Type) → Type
|
||||||
|
Sigma A B = Σ {A} B
|
||||||
|
|
||||||
|
syntax Sigma A (λ x → b) = Σ x ꞉ A , b
|
||||||
|
|
|
@ -0,0 +1,12 @@
|
||||||
|
open import general-notation
|
||||||
|
|
||||||
|
record 𝟙 : Type where
|
||||||
|
constructor
|
||||||
|
*
|
||||||
|
|
||||||
|
open 𝟙 public
|
||||||
|
|
||||||
|
𝟙-elim : {A : 𝟙 → Type}
|
||||||
|
→ A *
|
||||||
|
→ (x : 𝟙) → A x
|
||||||
|
𝟙-elim a * = a
|
|
@ -0,0 +1,7 @@
|
||||||
|
myLast :: [a] -> a
|
||||||
|
|
||||||
|
-- https://wiki.haskell.org/99_questions/Solutions/1
|
||||||
|
myLast [] = error "List empty"
|
||||||
|
|
||||||
|
myLast [x] = x
|
||||||
|
myLast (x:xs) = myLast xs
|
|
@ -0,0 +1,10 @@
|
||||||
|
-- Find second element from the end of a list
|
||||||
|
-- complete
|
||||||
|
|
||||||
|
myButLast :: [a] -> a
|
||||||
|
myButLast [] = error "List empty"
|
||||||
|
myButLast [x] = error "Single element list"
|
||||||
|
myButLast x = myButLastAux (reverse x)
|
||||||
|
|
||||||
|
myButLastAux :: [a] -> a
|
||||||
|
myButLastAux (x:xs:xss) = xs
|
|
@ -0,0 +1,8 @@
|
||||||
|
-- Find kth element in a list
|
||||||
|
-- complete
|
||||||
|
|
||||||
|
elementAt :: [a] -> Int -> a
|
||||||
|
|
||||||
|
elementAt [] k = error "no kth element"
|
||||||
|
elementAt (x:xs) k = if (k == 1) then x
|
||||||
|
else (elementAt xs (k-1))
|
|
@ -0,0 +1,6 @@
|
||||||
|
-- Find number of elements in a list.
|
||||||
|
-- ie, find length of the list.
|
||||||
|
|
||||||
|
myLength :: [a] -> Int
|
||||||
|
myLength [] = 0
|
||||||
|
myLength (_:xs) = 1 + (myLength xs)
|
|
@ -0,0 +1,5 @@
|
||||||
|
-- Reverse a list
|
||||||
|
|
||||||
|
myReverse :: [a] -> [a]
|
||||||
|
myReverse [] = []
|
||||||
|
myReverse (x:xs) = (myReverse xs) ++ [x]
|
|
@ -0,0 +1,10 @@
|
||||||
|
-- Check whether a list is a palindrome
|
||||||
|
-- incomplete
|
||||||
|
|
||||||
|
isPalindrome :: [a] -> bool
|
||||||
|
isPalindrome [] = []
|
||||||
|
isPalindrome [x] = x
|
||||||
|
isPalindrome (x:xs) = x == isPalindrome xs
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -0,0 +1,9 @@
|
||||||
|
-- Flatten list
|
||||||
|
-- incomplete
|
||||||
|
|
||||||
|
data NestedList a = Elem a
|
||||||
|
| List [NestedList a]
|
||||||
|
|
||||||
|
flatten :: NestedList -> list
|
||||||
|
flatten
|
||||||
|
|
|
@ -0,0 +1,20 @@
|
||||||
|
-- Eliminate consecutive duplicates
|
||||||
|
-- incomplete
|
||||||
|
|
||||||
|
{-
|
||||||
|
compress :: [a] -> [a]
|
||||||
|
|
||||||
|
compress [] = []
|
||||||
|
compress (x:xs:xss) =
|
||||||
|
-}
|
||||||
|
|
||||||
|
compressAux :: a -> [a] -> a
|
||||||
|
compressAux elem [] = elem
|
||||||
|
compressAux elem [x] = elem
|
||||||
|
compressAux elem (x:xs)
|
||||||
|
|
||||||
|
f aabbcc
|
||||||
|
(x:xs:xss) if x == xs then
|
||||||
|
|
||||||
|
|
||||||
|
-- aaaabccaadeee
|
|
@ -0,0 +1 @@
|
||||||
|
99 haskell problems
|
Loading…
Reference in New Issue