{- Programación con Tipos Dependientes Día 1 Mauro Jaskelioff basado en día 1 del curso de Thorsten Altenkirch en Rosario, 2011. -} module IntroEj where {- Empezamos con programación en Agda desde cero. -} {- Agda tiene muy pocos caracteres especiales y un lexer simple En principio, (){} separan cosas,pero el resto debe separado por espacios. -} {- Hete aquí los números naturales -} data ℕ : Set where zero : ℕ suc : (n : ℕ) → ℕ {- C-c C-l ejecuta el type checker. -} {- ℕ = \bn, → = \to -} {- Los siguientes pragmas nos permiten escribir decimales en lugar de suc (suc (.... )) -} {-# BUILTIN NATURAL ℕ #-} {-# BUILTIN ZERO zero #-} {-# BUILTIN SUC suc #-} _+_ : ℕ → ℕ → ℕ zero + n = n suc y + n = suc (y + n) {- C-c C-c divide en casos -} {- C-c C-r refina el problema -} {- podemos buscar una definición usando M-click -} {- evaluar usando C-c C-n -} {- Hacer la multiplicación -} _*_ : ℕ → ℕ → ℕ m * n = {!!} infixl 6 _+_ infixl 7 _*_ data Bool : Set where tt : Bool ff : Bool {- Escribir una función que decida la igualdad de los números naturales, eq m n = tt, si m=n eq m n = ff, en otro caso -} eq : ℕ → ℕ → Bool eq zero zero = tt eq zero (suc y) = ff eq (suc y) zero = ff eq (suc y) (suc y') = tt {- definimos las listas -} {- Declaramos asociatividad y precedencia del operador ∷ -} infixr 5 _∷_ data List (A : Set) : Set where [] : List A _∷_ : (x : A) → (xs : List A) → List A {- el guión bajo indica el lugar de los argumentos. Esta notación permite operadores mixfijos -} {- snoc agrega un elemento al final de la lista -} snoc : {A : Set} → List A → A → List A snoc [] a = a ∷ [] snoc (x ∷ xs) a = x ∷ snoc xs a {- C-c SPC chequea el tipo de lo que escribí. -} {- {A : Set} .. es un parámetro implícito, es inferido por el typechecker. -} {- dar vuelta una lista -} rev : {A : Set} → List A → List A rev [] = [] rev (x ∷ xs) = snoc (rev xs) x {- concatenar dos listas -} _++_ : {A : Set} → List A → List A → List A xs ++ ys = {!!} infixr 4 _++_ {- aplicación punto a punto -} appL : {A B : Set} → List (A → B) → List A -> List B appL [] xs = [] appL (f ∷ fs) [] = [] appL (f ∷ fs) (x ∷ xs) = f x ∷ appL fs xs {- Definimos el tipo Maybe -} data Maybe (A : Set) : Set where nothing : Maybe A just : A -> Maybe A {- devolver el elemento enésimo de una lista. -} _!!_ : {A : Set} → List A → ℕ → Maybe A [] !! n = nothing (x ∷ xs) !! zero = just x (x ∷ xs) !! suc n = xs !! n {- Chequeos dinámicos? Mejor usamos tipos más precisos! -} {- Definimos los vectores -} data Vec (A : Set) : ℕ → Set where [] : Vec A 0 _∷_ : {n : ℕ} → (x : A) → (xs : Vec A n) → Vec A (suc n) {- Aplica una función a todos los elementos del vector -} mapVec : ∀ {n} {A : Set} {B : Set} → (A → B) → Vec A n → Vec B n mapVec f [] = [] mapVec f (x ∷ xs) = (f x) ∷ (mapVec f xs) {- agrega un elemento al final del vector -} snoc' : {A : Set}{n : ℕ} → Vec A n → A → Vec A (suc n) snoc' [] a = a ∷ [] snoc' (x ∷ xs) a = x ∷ (snoc' xs a) {- invierte el orden de los elementos de un vector -} rev' : {A : Set}{n : ℕ} → Vec A n → Vec A n rev' [] = [] rev' (x ∷ xs) = snoc' (rev' xs) x {- El tipo Fin n me representa el conjunto {0,1,...,n-1} -} data Fin : ℕ -> Set where zero : {n : ℕ} → Fin (suc n) suc : {n : ℕ} → Fin n -> Fin (suc n) {- Un vector con los elementos de Fin, en orden -} enum : (n : ℕ) → Vec (Fin n) n enum zero = [] enum (suc n) = zero ∷ (mapVec suc (enum n)) {- elemento máximo de un conjunto de tipo Fin (suc n) -} max : {n : ℕ} → Fin (suc n) max {zero} = zero max {suc n} = suc max {- nat : da el natural correspondiente a un elemento de Fin n -} nat : {n : ℕ} → Fin n → ℕ nat zero = zero nat (suc n) = suc (nat n) {- emb inserta un elemento de Fin n en Fin (suc n) de manera tal que nat x = nat (emb x) -} emb : {n : ℕ} → Fin n → Fin (suc n) emb n = {!!} {- inv me lleva de {0,1,...,n-1} a {n-1,..,1,0} -} inv : {n : ℕ} → Fin n → Fin n inv n = {!!} {- proyección para vectores -} _!!'_ : {A : Set}{n : ℕ} → Vec A n → Fin n → A [] !!' () (x ∷ xs) !!' zero = x (x ∷ xs) !!' suc n = xs !!' n {- aplicación punto a punto para vectores -} appV : {A B : Set}{n : ℕ} → Vec (A → B) n → Vec A n → Vec B n appV [] [] = [] appV (f ∷ fs) (x ∷ xs) = (f x) ∷ (appV fs xs) {- Estáticamente aseguramos que la proyección está bien definida! -} Vector : ℕ → Set {- Vec n es un vector n-dimensional -} Vector m = Vec ℕ m Matrix : ℕ → ℕ → Set {- Matrix m n es una matriz de m x n -} Matrix m n = Vec (Vector n) m {- multiplicación por un escalar -} _*v_ : {n : ℕ} → ℕ → Vector n → Vector n k *v ms = {!!} v1 : Vector 3 v1 = 1 ∷ 2 ∷ 3 ∷ [] test1 : Vector 3 test1 = 2 *v v1 {- suma de vectores -} _+v_ : {n : ℕ} → Vector n → Vector n → Vector n v1 +v v2 = {!!} v2 : Vector 3 v2 = 2 ∷ 3 ∷ 0 ∷ [] test2 : Vector 3 test2 = v1 +v v2 {- multiplicación de un vector y una matriz -} _*vm_ : {m n : ℕ} → Vector m → Matrix m n → Vector n v *vm m = {!!} id3 : Matrix 3 3 id3 = (1 ∷ 0 ∷ 0 ∷ []) ∷ (0 ∷ 1 ∷ 0 ∷ []) ∷ (0 ∷ 0 ∷ 1 ∷ []) ∷ [] test3 : Vector 3 test3 = v1 *vm id3 {- multiplicación de matrices -} _*mm_ : {l m n : ℕ} → Matrix l m → Matrix m n → Matrix l n m1 *mm m2 = {!!} inv3 : Matrix 3 3 inv3 = (0 ∷ 0 ∷ 1 ∷ []) ∷ (0 ∷ 1 ∷ 0 ∷ []) ∷ (1 ∷ 0 ∷ 0 ∷ []) ∷ [] test4 : Matrix 3 3 test4 = inv3 *mm inv3 {- transposición de matrices -} transpose : {n m : ℕ} → Matrix m n → Matrix n m transpose m = {!!} ej5 : Matrix 3 3 ej5 = ( 0 ∷ 1 ∷ 2 ∷ []) ∷ ( 3 ∷ 4 ∷ 5 ∷ []) ∷ ( 6 ∷ 7 ∷ 8 ∷ []) ∷ [] test5 : Matrix 3 3 test5 = transpose ej5