El sistema de tipos de Haskell | 1/5

Guillaume Hoffmann

Presentaciones

Su humilde servidor

¿Porqué este curso?

Porqué Haskell

El temido piramide de Haskell

^    más complejo
|   
|         / \          <- lo que se publica en internet
|        /   \
|       /     \ 
|      /       \       <- poco material de eso
|     /         \ 
|    /           \
|   /             \    <- lo que hay que saber para empezar
|   ---------------
|   
|    menos complejo

Ustedes

¿Quiénes son? :)

Este curso supone que ya saben:

Y no cubre:

Contenido / Plan

  1. Lunes: tipos, clases de tipos, Monoid
  2. Martes: IO, Functor, Applicative, Monad, newtype
  3. Miércoles: multiclases, functional dependencies, type families
  4. Jueves: GADTs, tipos fantasmas, tipos existenciales
  5. Viernes: RankNTypes, DataKinds, TypeInType

Para qué necesitamos a los sistemas de tipos

Los sistemas de tipos sirven para hacer programas correctos e impedir que se puedan representar estados incorrectos.

Julie Moroniki - Haskell Programming from first principles

“A type system is a tractable syntactic method of proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.”

Benjamin Pierce - Types and Programming Languages

Día 1

Temas

Preparándonos

Machete GHCi

ghci es el intérprete, ghc el compilador.

Uso básico de GHCi

Evaluar expresiones y mostrar su valor:

> 10 + 12
22

> "Hola" ++ " mundo"
"Hola mundo"

> words "Hola mundo"
["Hola","Mundo"]

> map show "abcdefg"
["'a'","'b'","'c'","'d'","'e'","'f'","'g'"]

Anotaciones de tipo

> :t "Hola"
"Hola" :: [Char]

> :t []
[] :: [a]

> :t [] ++ []
[] ++ [] :: [a]

> :t 10
10 :: Num p => p

Se pueden poner en código Haskell para precisar algun tipo:

> :t [] :: [Int]
[] :: [Int] :: [Int]

> :t 10 :: Integer
10 :: Integer :: Integer

Huecos tipados

> [_] :: [Int]

<interactive>:10:2: error:
    • Found hole: _ :: Int
    • In the expression: _
      In the expression: [_] :: [Int]
      In an equation for ‘it’: it = [_] :: [Int]
    • Relevant bindings include
        it :: [Int] (bound at <interactive>:10:1)

Probar:

> _ :: Int
> _ :: Maybe Char
> _ :: Int Char
> _ :: Maybe Maybe

Inferencia de tipos

Haskell tiene inferencia de tipos.

No hace falta indicar todos los tipos de las funciones porque los tipos conocidos se propagan al resto del código.

El mecanismo de esa propagación es la unificación.

Unificación

Algoritmo nacido en lógica (usado en lógica de primer orden por ejemplo).

Dados dos términos conteniendo alguna variable, encontrar, si existe, la sustitución más simple (es decir, una asignación de algún termino a cada variable) que hace iguales a los dos términos. La sustitución resultante se llama unificador más general (most general unifier).

Terminos unificables:

Terminos no unificables:

Errores de tipeo

Prelude> (1 :: Int) +  (10 :: Integer)

<interactive>:3:16: error:
    • Couldn't match expected type ‘Int’ with actual type ‘Integer’
    • In the second argument of ‘(+)’, namely ‘(10 :: Integer)’
      In the expression: (1 :: Int) + (10 :: Integer)
      In an equation for ‘it’: it = (1 :: Int) + (10 :: Integer)

Cuando falla la unificación, tenemos un error de tipeo. GHC nos informa la discrepancia entre tipo esperado y tipo encontrado.

Esos mensages pueden ser más complejos que en un lenguaje sin inferencia de tipos.

Porque el lugar donde la unificación falla no es siempre donde intuitivamente está el error.

Ejemplos de inferencia de tipos con unificacion

map f [] = []
map f (first:rest) = f first : map f rest

Tipos de datos algebraicos (palabra-clave data)

Sobrecarga de funciones

En programación, suele pasar que queremos sobrecarga de algunas funciones = un mismo nombre de función con distintas implementaciones según el contexto:

¿Cómo integrar bien la sobrecarga en un lenguaje como Haskell?

Solucion en Haskell:

la sobrecarga se debería reflejar en el tipo de una función

Y así nacieron las clases de tipos.

Repaso de clases de tipos conocidas

Ejecutar en GHCi:

> :info Eq
> :info Ord
> :info Num

Observamos:

Ejemplos de clases de tipos

class Eq a where
  (==) :: a -> a -> Bool
  (/=) :: a -> a -> Bool

Función usando sobrecarga:

member :: Eq a => a -> [a] -> Bool
member x []                 = False
member x (y:ys) | x==y      = True
                | otherwise = member x ys

Definiendo instancias

data Coord = Coord Int Int

instance Eq Coord where
  C x1 y1 == C x2 y2 = x1 == x2 && y1 == y2
  c1 /= c2 = not (c1 == c2)

Instancia para tipo polimórfico:

instance (Eq a) => Eq [a] where
  []     == []     = True
  (x:xs) == (y:ys) = (x == y) && (xs == ys)
  xs     /= ys     = not (xs == ys)

Ejercicio

¿Los polinomios pueden ser números?

Veamos el práctico.

La clase Monoid

class Monoid a where
  mempty :: a
  mappend :: a -> a -> a
  mconcat :: [a] -> a
  {-# MINIMAL mempty, mappend #-}

Las instancias de Monoid deben seguir ciertas leyes:

mappend mempty x = x

mappend x mempty = x

mappend x (mappend y z) = mappend (mappend x y) z

mconcat = foldr mappend mempty

Instancias y modulos Haskell

En Haskell, las instancias no tienen nombre.

Cuando se importa un módulo M, se importan todas las instancias definidas adentro, no se puede elegir cuáles:

Instancias huerfanas

hay 3 lugares posibles para definir una instancia C T:

El último caso es el caso de una instancia huérfana. GHC emite un warning cuando encuentra una.

Porqué hay que evitar las Instancias Huerfanas

Porque puede haber colisiones de instancias para un mismo par C y T.

Recordar que no se pueden excluir instancias cuando se importa un módulo.

Si se esta diseñando una libreria, esta mal visto tener instancias huerfanas.

Atenta a la modularidad de las librerias.

Si es una aplicacion, cierta gente las tolera.

Otros lenguajes las prohiben directamente (PureScript).

Para saber mas sobre ese debate

Porqué permitir importar explicitamente puede causar problemas:

https://stackoverflow.com/questions/8728596/explicitly-import-instances/8731340#8731340

Conclusiones

Para mañana: