diff --git a/Main.pdf b/Main.pdf index 6613bb0c65590984b1b0c9e6f135ce6c5d8ac860..9c05a75a150b058bcd2a7954b0e9397c007bdb7e 100644 Binary files a/Main.pdf and b/Main.pdf differ diff --git a/bib.bib b/bib.bib index 3ec383135db49fe70ef78062ee9ad886e2fe4eaa..569128a4e0a4aa7c924848de0e1a447e8c743d31 100644 --- a/bib.bib +++ b/bib.bib @@ -90,3 +90,22 @@ howpublished = {http://okmij.org/ftp/Computation/lambda-calc.html}, note = {Accedido: 28-5-2018} } + + +@inproceedings{Yorgey:2012:GHP:2103786.2103795, + author = {Yorgey, Brent A. and Weirich, Stephanie and Cretin, Julien and Peyton Jones, Simon and Vytiniotis, Dimitrios and Magalh\~{a}es, Jos{\'e} Pedro}, + title = {Giving Haskell a Promotion}, + booktitle = {Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation}, + series = {TLDI '12}, + year = {2012}, + isbn = {978-1-4503-1120-5}, + location = {Philadelphia, Pennsylvania, USA}, + pages = {53--66}, + numpages = {14}, + url = {http://doi.acm.org/10.1145/2103786.2103795}, + doi = {10.1145/2103786.2103795}, + acmid = {2103795}, + publisher = {ACM}, + address = {New York, NY, USA}, + keywords = {haskell, kinds, polymorphism, promotion}, +} diff --git a/src/New.lhs b/src/New.lhs index dc227eab263270d583b5fe053dce63ea5b4188ba..98418960db0bef9fc1202cc99fe5a41d6f434aec 100644 --- a/src/New.lhs +++ b/src/New.lhs @@ -1,11 +1,96 @@ %if False +> {-# LANGUAGE DataKinds #-} +> {-# LANGUAGE FlexibleContexts #-} +> {-# LANGUAGE GADTs #-} +> {-# LANGUAGE KindSignatures #-} +> {-# LANGUAGE PatternSynonyms #-} +> {-# LANGUAGE Rank2Types #-} +> {-# LANGUAGE ScopedTypeVariables #-} +> {-# LANGUAGE TypeFamilies #-} +> {-# LANGUAGE TypeOperators #-} +> {-# LANGUAGE FlexibleInstances #-} +> {-# LANGUAGE UndecidableInstances #-} +> {-# LANGUAGE MultiParamTypeClasses #-} +> {-# LANGUAGE PolyKinds #-} + + %endif + \subsubsection{TypeFamilies} + +INTRO + +Algunas definiciones posibles: + + + + \subsubsection{DataKinds} +Con el desarrollo del concepto de datatype promotion +~\cite{Yorgey:2012:GHP:2103786.2103795} +es un importante salto de expresividad. En lugar de tener un sistema +de kinds en donde solamente se logra expresar la aridad de los tipos, +pueden \emph{promoverse} datatypes adecuados. + +Con la extensi\'on {\tt -XDataKinds}, cada declaraci\'on de tipos como + +> data Nat = Zero | Succ Nat + +se duplica a nivel de Kinds. + +Adem\'as de introducir los t\'erminos {\tt Zero} y {\tt Succ} de tipo +{\tt Nat}, y al propio tipo {\tt Nat } de kind {\tt *}, introduce +los TIPOS {\tt Zero} y {\tt Succ} de Kind {\tt Nat} (y al propio kind Nat). + +El kind {\tt *} pasa entonces a ser el de los tipos habitados, y cada vez que +declaramos un tipo promovible se introducen tipos no habitados del nuevo kind. + + +En el ejemplo de la secci\'on anterior, el tipo {\tt Vec } ten\'ia kind +{\tt * $\rightarrow$ * $\rightarrow$ *} por lo que {\tt Vec Bool Char} +era un tipo v\'alido. +Con DataKinds podemos construir: (+KindSignatures para anotar) + +> data Vec :: Nat -> * -> * where +> VZ :: Vec Zero a +> VS :: a -> Vec n a -> Vec (Succ n) a + +\subsubsection{{\tt GHC.TypeLits}} + +intro del modulo + +Usando {\tt GHC.TypeLits} podemos escribir: (+TypeOperators) + +< data Vec :: Nat -> * -> * where +< VZ :: Vec 0 a +< VS :: a -> Vec n a -> Vec (n+1) a + +Podemos entonces implementar funciones seguras con estos tipos +"dependientes". + +< data Proxy (n :: k) = Proxy --PolyKinds + +> vHead :: Vec (Succ n) a -> a +> vHead (VS a _) = a + +> vTail :: Vec (Succ n) a -> Vec n a +> vTail (VS _ as) = as + +> vZipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c +> vZipWith _ VZ VZ = VZ +> vZipWith f (VS x xs) (VS y ys) +> = VS (f x y)(vZipWith f xs ys) + +COMENTAR TOTALIDAD, safety + +MAS EJEMPLOS? + \subsubsection{Proxys y Singletons} + +