Linear Types

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

:!stack build linear-base

{-# LANGUAGE LinearTypes #-}

{-# LANGUAGE NoImplicitPrelude #-}

import Prelude.Linear

Intuición

id :: a -> a
id x = x

id :: a %1 -> a
id x = x

id 'a'

Redundant id

Found:

id 'a'

Why Not:

'a'

'a'

dup :: a -> (a, a)
dup x = (x, x)

dup' :: a %1 -> (a, a)
dup' x = (x, x)

<interactive>:4:6: error:
    • Couldn't match type ‘'Many’ with ‘'One’ arising from multiplicity of ‘x’
    • In an equation for ‘dup'’: dup' x = (x, x)

Consumo lineal:

• Para consumir linealmente un término de un tipo base atómico, el término debe ser evaluado. Esto incluye tipos como Int, Char, Float.
• Para consumir una función linealmente, se debe aplicar la función a un argumento, y consumir su resultado exactamente una vez.
• Para consumir un par (tupla de dos entradas), se debe realizar la coincidencia de patrones y consumir cada entrada exactamente una vez.
• En general, para consumir linealmente un término que corresponde a un tipo de dato algebráico, se debe realizar la coincidencia de patrones y consumir cada entrada con multiplicidad lineal exactamente una vez.

:t (+)

(+) :: forall a. Additive a => a %1 -> a %1 -> a

:t (*)

(*) :: forall a. Multiplicative a => a %1 -> a %1 -> a

:t fst

fst :: forall a b. (a, b) -> a

swap :: (a, b) -> (b, a)
swap (x,y) = (y,x)

swap' :: (a, b) %1 -> (b, a)
swap' (x,y) = (y,x)

:t swap
:t swap'

swap :: forall a b. (a, b) -> (b, a)

swap' :: forall a b. (a, b) %1 -> (b, a)

Tipos de Datos

data Par a b = Par a b

:t Par

swapPar :: Par a b %1 -> Par b a
swapPar (Par x y) = Par x x

:t swapPar

data List a = Empty | Cons a (List a)

head :: List a %1 -> a
head Empty = error "Vacía"
head (Cons x xs) = x