Generalised Algebraic Data Types

Juan Pablo Yamamoto
jpyamamoto[at]ciencias.unam.mx
Lógica Computacional II. Semestre 2025-1.

Requisitos Previos

{-# LANGUAGE GADTs #-}

Codificación de Naturales como Tipos

Codificamos los tipos naturales al nivel de tipos, no nos interesa que tengamos términos que los representen (constructores).

data Zero
data Succ n

Vectores

Teniendo números naturales, podemos codificar los vectores como listas dependientes de un natural.

• Un vector es una lista de tamaño fijo y finito.
• Vector vacío
• Dado un vector xs de tamaño n, Cons x xs es un vector de tamaño n+1

data Vec a n where
    Void :: Vec a Zero
    Cons :: a -> Vec a n -> Vec a (Succ n)

instance Show a => Show (Vec a n) where
    show Void = "Void"
    show (Cons x xs) = "(Cons " ++ show x ++ " " ++ show xs ++ ")"

:t Void

Void :: forall a. Vec a Zero

:t Cons 1 Void
:t Cons 1 (Cons 2 Void)

Cons 1 Void :: forall {a}. Num a => Vec a (Succ Zero)

Cons 1 (Cons 2 Void) :: forall {a}. Num a => Vec a (Succ (Succ Zero))

Funciones seguras

Definición de head:

headVec :: Vec a (Succ n) -> a
headVec (Cons x _) = x

:t headVec (Cons 1 Void)

headVec (Cons 1 Void) :: forall {a}. Num a => a

:t headVec Void

<interactive>:1:9: error:
    • Couldn't match type ‘Zero’ with ‘Succ n0’
      Expected: Vec a (Succ n0)
        Actual: Vec a Zero
    • In the first argument of ‘headVec’, namely ‘Void’
      In the expression: headVec Void

:t head []

head [] :: forall {a}. a

head []

Prelude.head: empty list
CallStack (from HasCallStack):
  error, called at libraries/base/GHC/List.hs:1646:3 in base:GHC.List
  errorEmptyList, called at libraries/base/GHC/List.hs:85:11 in base:GHC.List
  badHead, called at libraries/base/GHC/List.hs:81:28 in base:GHC.List
  head, called at <interactive>:1:1 in interactive:Ghci169

Definición de tail:

tailVec :: Vec a (Succ n) -> Vec a n
tailVec (Cons _ xs) = xs

:t tailVec (Cons 1 Void)

tailVec (Cons 1 Void) :: forall {a}. Num a => Vec a Zero

:t tailVec Void

<interactive>:1:9: error:
    • Couldn't match type ‘Zero’ with ‘Succ n’
      Expected: Vec a (Succ n)
        Actual: Vec a Zero
    • In the first argument of ‘tailVec’, namely ‘Void’
      In the expression: tailVec Void

:t tail []

tail [] :: forall {a}. [a]

tail []

Prelude.tail: empty list
CallStack (from HasCallStack):
  error, called at libraries/base/GHC/List.hs:1646:3 in base:GHC.List
  errorEmptyList, called at libraries/base/GHC/List.hs:128:28 in base:GHC.List
  tail, called at <interactive>:1:1 in interactive:Ghci237

Definición de map:

mapVec :: (a -> b) -> Vec a n -> Vec b n
mapVec f Void = Void
mapVec f (Cons x xs) = Cons (f x) (mapVec f xs)

Append

¿Cuál sería el tipo que corresponde?

append :: Vec a m -> Vec a n -> Vec a ???

Suma de Naturales

data Sum m n s where
    SumZero :: Sum Zero n n
    SumSucc :: Sum m n s -> Sum (Succ m) n (Succ s)

instance Show (Sum m n s) where
    show SumZero = "SumZero"
    show (SumSucc n) = "(SumSucc " ++ show n ++ ")"

Damos evidencia de los tipos, para definir la suma.

append :: Sum m n s -> Vec a m -> Vec a n -> Vec a s
append SumZero Void ys = ys
append (SumSucc p) (Cons x xs) ys = Cons x (append p xs ys)

append SumZero Void (Cons 2 Void)

(Cons 2 Void)

:t SumSucc SumZero

SumSucc SumZero :: forall {s}. Sum (Succ Zero) s (Succ s)

append (SumSucc (SumSucc SumZero)) (Cons 1 (Cons 2 (Cons 3 Void))) (Cons 4 Void)

<interactive>:1:53: error:
    • Couldn't match type ‘Succ Zero’ with ‘Zero’
      Expected: Vec a Zero
        Actual: Vec a (Succ Zero)
    • In the second argument of ‘Cons’, namely ‘(Cons 3 Void)’
      In the second argument of ‘Cons’, namely ‘(Cons 2 (Cons 3 Void))’
      In the second argument of ‘append’, namely ‘(Cons 1 (Cons 2 (Cons 3 Void)))’

fromList :: [a] -> Vec a n
fromList [] = Void
fromList (x:xs) = Cons x (fromList xs)

Use foldr

Found:

fromList [] = Void fromList (x : xs) = Cons x (fromList xs)

Why Not:

fromList xs = foldr Cons Void xs

<interactive>:2:15: error:
    • Couldn't match type ‘n’ with ‘Zero’
      Expected: Vec a n
        Actual: Vec a Zero
      ‘n’ is a rigid type variable bound by
        the type signature for:
          fromList :: forall a n. [a] -> Vec a n
        at <interactive>:1:1-26
    • In the expression: Void
      In an equation for ‘fromList’: fromList [] = Void
    • Relevant bindings include fromList :: [a] -> Vec a n (bound at <interactive>:2:1)