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

Tipos de Datos

data Par a b = Par a b

:t Par

Par :: forall a b. a -> b -> Par a b

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

:t swapPar

swapPar :: forall a b. Par a b %1 -> Par b a

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

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

Unrestricted

data Unrestricted a where
    Unr :: a -> Unrestricted a

longitudLista :: List a %1 -> (Unrestricted Int, List a)
longitudLista Empty = (Unr 0, Empty)
longitudLista (Cons x xs) = case longitudLista xs of
    (Unr n, xs') -> (Unr (n+1), Cons x xs')

ignoreLongitud :: List a %1 -> List a
ignoreLongitud l = case longitudLista l of
    (Unr _, l') -> l'

:i Ur

type Ur :: * -> * data Ur a where Ur :: a -> Ur a -- Defined in ‘Data.Unrestricted.Linear.Internal.Ur’ instance IHaskellPrelude.Foldable Ur -- Defined in ‘Data.Unrestricted.Linear.Internal.Ur’ instance IHaskellPrelude.Traversable Ur -- Defined in ‘Data.Unrestricted.Linear.Internal.Ur’ instance IHaskellPrelude.Applicative Ur -- Defined in ‘Data.Unrestricted.Linear.Internal.Ur’ instance IHaskellPrelude.Functor Ur -- Defined in ‘Data.Unrestricted.Linear.Internal.Ur’ instance IHaskellPrelude.Monad Ur -- Defined in ‘Data.Unrestricted.Linear.Internal.Ur’ instance IHaskellPrelude.Eq a => Eq (Ur a) -- Defined in ‘Data.Ord.Linear.Internal.Eq’ instance IHaskellPrelude.Ord a => Ord (Ur a) -- Defined in ‘Data.Ord.Linear.Internal.Ord’ instance Consumable (Ur a) -- Defined in ‘Data.Unrestricted.Linear.Internal.Consumable’ instance Dupable (Ur a) -- Defined in ‘Data.Unrestricted.Linear.Internal.Dupable’ instance Movable (Ur a) -- Defined in ‘Data.Unrestricted.Linear.Internal.Movable’

Arreglos

import qualified Data.Array.Mutable.Linear as Array

:t Array.alloc

Array.alloc :: forall a b. HasCallStack => Int -> a -> (Array a %1 -> Ur b) %1 -> Ur b

:t Array.set

Array.set :: forall a. HasCallStack => Int -> a -> Array a %1 -> Array a

:t Array.get

Array.get :: forall a. HasCallStack => Int -> Array a %1 -> (Ur a, Array a)

:t Array.freeze

Array.freeze :: forall a. Array a %1 -> Ur (Vector a)

:t ($)
:t (&)

($) :: forall a b (p :: Multiplicity) (q :: Multiplicity). (a %p -> b) %q -> a %p -> b

(&) :: forall a b (p :: Multiplicity) (q :: Multiplicity). a %p -> (a %p -> b) %q -> b

($) f x = f x
(&) x f = f x

sumArray :: Num a => Array.Array a %1 -> (Ur a, Array.Array a)
sumArray a = Array.size a &
    \(Ur n, a') -> sumArray' (n-1) (fromInteger 0) a'

sumArray' :: Num a => Int -> a -> Array.Array a %1 -> (Ur a, Array.Array a)
sumArray' i s a
    | i < 0 = (Ur s, a)
    | otherwise = Array.get i a & \(Ur x, a') -> sumArray' (i-1) (s+x) a'

Redundant fromInteger

Found:

fromInteger 0

Why Not:

0

Ur (n, v) = Array.alloc 10 (0 :: Int) (\a -> sumArray a & 
                                        \(Ur n, a') -> Array.freeze a' &
                                         \(Ur v) -> Ur (n, v))

(n, v)

(0,[0,0,0,0,0,0,0,0,0,0])

Ur (n', v') = Array.fromList ([0..10] :: [Int]) (\a -> sumArray a &
                                                  \(Ur n, a') -> Array.freeze a'&
                                                    \(Ur v) -> Ur (n, v))

(n', v')

(55,[0,1,2,3,4,5,6,7,8,9,10])