Esiste un modo per emulare i tipi lineari in Haskell?

Question

Sto modellando un sistema che ha un'operazione che crea una risorsa e altre operazioni che consumano quella risorsa. Tuttavia, una determinata risorsa può essere consumata solo una volta - c'è un modo che posso garantire al momento della compilazione?

Per concretezza, diciamo che la prima operazione cuoce una torta e che ci sono altre due operazioni, una per "scegliere di mangiare" la torta e una per "scegliere di avere la torta" e che posso fare solo una o l'altro.

-- This is my current "weakly typed" interface: 
bake :: IO Cake 
eat :: Cake -> IO() 
keep :: Cake -> IO() 

-- This is OK 
do 
    brownie <- bake 
    muffin <- bake 
    eat brownie 
    keep muffin 

-- Eating and having the same cake is not OK: 
do 
    brownie <- bake 
    eat brownie 
    keep brownie -- oops! already eaten! 

sua facile da applicare la limitazione di non mantenere una torta già mangiata (o viceversa) in fase di esecuzione impostando una bandiera sulla torta dopo lo usiamo. Ma c'è un modo per far rispettare questo in fase di compilazione?

BTW, questa domanda è pensata per una dimostrazione del concetto, quindi sono d'accordo con qualsiasi magia nera che possa darmi la sicurezza statica che voglio.

Answer 1

In Haskell, una versione base di questo potrebbe essere espresso con un GADT indicizzato da un negozio di dolci (rappresentata da un elenco di Nat -s):

{-# LANGUAGE 
    TypeFamilies, GADTs, TypeOperators, PartialTypeSignatures, 
    DataKinds, PolyKinds #-} 

import GHC.TypeLits 
import Data.Proxy 
import GHC.Exts 

-- Allocate a new cake 
type family New cs where 
    New '[]  = 0 
    New (c ': cs) = c + 1 

-- Constraint satisfiable if "c" is in "cs" 
type family Elem c cs :: Constraint where 
    Elem c (c ': cs) =() 
    Elem c (c' ': cs) = Elem c cs 

type family Remove c cs where 
    Remove c '[]  = '[] 
    Remove c (c ': cs) = cs 
    Remove c (c' ': cs) = c' ': Remove c cs 

data Bake :: [Nat] -> [Nat] -> * -> * where 
    Pure :: a -> Bake cs cs a 
    Bake :: (Proxy (New cs) -> Bake (New cs ': cs) cs' a) -> Bake cs cs' a 
    Eat :: Elem c cs => Proxy c -> Bake (Remove c cs) cs' a -> Bake cs cs' a 
    Keep :: Elem c cs => Proxy c -> Bake cs cs' a -> Bake cs cs' a 

ok :: Bake '[] _ _ 
ok = 
    Bake $ \cake1 -> 
    Bake $ \cake2 -> 
    Eat cake1 $ 
    Keep cake2 $ 
    Eat cake2 $ 
    Pure() 

not_ok :: Bake '[] _ _ 
not_ok = 
    Bake $ \cake1 -> 
    Bake $ \cake2 -> 
    Eat cake1 $ 
    Keep cake1 $ -- we already ate that 
    Eat cake2 $ 
    Pure() 

Non è possibile rimuovere il tipo annotazioni da Bake azioni e lasciare tipi di dedurre:

foo = 
    Bake $ \cake1 -> 
    Bake $ \cake2 -> 
    Eat cake1 $ 
    Pure() 

-- Error: Could not deduce (Elem (New cs0) (New cs0 + 1 : New cs0 : cs0)) 

Ovviamente, (Elem (New cs0) (New cs0 + 1 : New cs0 : cs0)) è soddisfacibile per tutti cs0, ma GHC non possono vedere questo, perché non può decidere se New cs0 non è uguale a New cs0 + 1, perché GHC non può assumere nulla sulla variabile flessibile cs0.

Se aggiungiamo NoMonomorphismRestriction, foo digiterebbe typececk, ma ciò farebbe sì che anche i programmi errati digitassero premendo tutti i vincoli Elem in alto. Ciò impedirebbe comunque di fare qualcosa di utile con i termini sbagliati, ma è una soluzione piuttosto brutta.

---

Più in generale, possiamo esprimere Bake come una monade libera indicizzato, che ci fa do -notation con RebindableSyntax, e permette una definizione per BakeF che è un po 'più chiaro di quello che abbiamo visto prima. Potrebbe anche ridurre il boilerplate in modo molto simile alla semplice monade Free, anche se trovo piuttosto improbabile che le persone trovino uso per le monad indicizzate gratuite in due diverse occasioni nel codice pratico.

{-# LANGUAGE 
    TypeFamilies, GADTs, TypeOperators, PartialTypeSignatures, StandaloneDeriving, 
    DataKinds, PolyKinds, NoImplicitPrelude, RebindableSyntax, DeriveFunctor #-} 

import Prelude hiding (Monad(..)) 
import GHC.TypeLits 
import Data.Proxy 
import GHC.Exts 

class IxFunctor f where 
    imap :: (a -> b) -> f i j a -> f i j b 

class IxFunctor m => IxMonad m where 
    return :: a -> m i i a 
    (>>=) :: m i j a -> (a -> m j k b) -> m i k b 
    fail :: String -> m i j a 

infixl 1 >> 
infixl 1 >>= 

(>>) :: IxMonad m => m i j a -> m j k b -> m i k b 
ma >> mb = ma >>= const mb 

data IxFree f i j a where 
    Pure :: a -> IxFree f i i a 
    Free :: f i j (IxFree f j k a) -> IxFree f i k a 

liftf :: IxFunctor f => f i j a -> IxFree f i j a 
liftf = Free . imap Pure 

instance IxFunctor f => IxFunctor (IxFree f) where 
    imap f (Pure a) = Pure (f a) 
    imap f (Free fa) = Free (imap (imap f) fa) 

instance IxFunctor f => IxMonad (IxFree f) where 
    return = Pure 
    Pure a >>= f = f a 
    Free fa >>= f = Free (imap (>>= f) fa) 
    fail = error 

-- Old stuff for Bake 

type family New cs where 
    New '[]  = 0 
    New (c ': cs) = c + 1 

type family Elem c cs :: Constraint where 
    Elem c (c ': cs) =() 
    Elem c (c' ': cs) = Elem c cs 

type family Remove c cs where 
    Remove c '[]  = '[] 
    Remove c (c ': cs) = cs 
    Remove c (c' ': cs) = c' ': Remove c cs 

-- Now the return type indices of BakeF directly express the change 
-- from the old store to the new store. 
data BakeF cs cs' k where 
    BakeF :: (Proxy (New cs) -> k) -> BakeF cs (New cs ': cs) k 
    EatF :: Elem c cs => Proxy c -> k -> BakeF cs (Remove c cs) k 
    KeepF :: Elem c cs => Proxy c -> k -> BakeF cs cs k 

deriving instance Functor (BakeF cs cs') 
instance IxFunctor BakeF where imap = fmap 

type Bake = IxFree BakeF 

bake = liftf (BakeF id) 
eat c = liftf (EatF c()) 
keep c = liftf (KeepF c()) 

ok :: Bake '[] _ _ 
ok = do 
    cake1 <- bake 
    cake2 <- bake 
    eat cake1 
    keep cake2 
    eat cake2 

-- not_ok :: Bake '[] _ _ 
-- not_ok = do 
-- cake1 <- bake 
-- cake2 <- bake 
-- eat cake1 
-- keep cake1 -- already ate it 
-- eat cake2 

Answer 2

Una soluzione parziale. Potremmo definire un tipo di involucro

data Caked a = Caked { getCacked :: IO a } --^internal constructor 

di cui noi non esportiamo il costruttore/di accesso.

Sarebbe avere due funzioni quasi-ma-non-proprio-come-bind:

beforeCake :: IO a -> (a -> Caked b) -> Caked b 
beforeCake a f = Caked (a >>= getCaked . f) 

afterCake :: Caked a -> (a -> IO b) -> Caked b 
afterCake (Caked a) f = Caked (a >>= f) 

L'unico modo per i clienti per creare Caked valori sarebbero attraverso:

eat :: Cake -> Caked() 
eat = undefined 

keep :: Cake -> Caked() 
keep = undefined 

E noi allocherebbe Cake valori su un callback:

withCake :: (Cake -> Caked b) -> IO b 
withCake = undefined 

Questo, penso, assicurerebbe che eat e keep vengano richiamati solo una volta all'interno del callback.

Problemi: non funziona con più Cake allocazioni e Cake valori possono ancora sfuggire al campo di applicazione della richiamata (potrebbe phantom tipi aiuto qui?)

Answer 3

Polakow ha mostrato nel suo articolo Haskell Simposio Embedding a full linear lambda calculus in Haskell (pdf) come farlo.

L'idea principale è quella di indicizzare ogni costruttore con un input e un contesto di output che tiene traccia delle risorse consumate nei vari sottotemi.