Czy istnieje sposób na emulowanie typów liniowych w Haskell?

Question

Modeluję system, który ma operację, która tworzy zasób i inne operacje, które zużywają ten zasób. Jednak dany zasób może zostać zużyty tylko raz - czy istnieje sposób, który mogę zagwarantować podczas kompilacji?

Dla konkretności, powiedzmy, że pierwsza operacja upiecza ciasto i że są jeszcze dwie inne operacje, jedna dla "wyboru jedzenia" ciasta i jedna dla "wyboru ciasta" i że mogę zrobić tylko jedną lub inny.

-- 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! 

Łatwo wymusić ograniczenie nie kontrolując już zjedzone ciastko (lub odwrotnie) w czasie wykonywania przez ustawienie flagi na torcie po tym jak go używać. Ale czy istnieje sposób na wymuszenie tego podczas kompilacji?

BTW, to pytanie jest przeznaczone do sprawdzenia koncepcji, więc jestem w porządku z każdą czarną magią, która może zapewnić mi statyczne bezpieczeństwo, jakiego pragnę.

Answer 1

W Haskell, podstawowa wersja ta może być wyrażona za pomocą GADT indeksowane przez sklep ciast (reprezentowany przez listy 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() 

Niestety nie możemy usunąć typ adnotacje z Bake działań i pozostawić rodzaje należy wnioskować:

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

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

Oczywiście (Elem (New cs0) (New cs0 + 1 : New cs0 : cs0)) jest spe dla wszystkich cs0, ale GHC nie widzi tego, ponieważ nie może zdecydować, czy New cs0 jest nierówny do New cs0 + 1, ponieważ GHC nie może przyjąć nic na temat elastycznej zmiennej cs0.

Jeśli dodamy NoMonomorphismRestriction, będzie to typecheck, foo, ale spowoduje to, że nawet niepoprawne programy będą sprawdzać typowo, przesuwając wszystkie więzy Elem na górę. Wciąż uniemożliwiałoby to robienie czegokolwiek pożytecznego z niewłaściwymi terminami, ale jest to dość brzydkie rozwiązanie.

---

Bardziej ogólnie, możemy wyrazić Bake jako indeksowanego wolnego monady, które dostaje nam do -notation z RebindableSyntax i umożliwia definicję BakeF który jest nieco jaśniejsze niż to, co widzieliśmy wcześniej. Mogłoby to również zredukować charakterystykę podstawową podobnie jak zwykłą monadę Free, chociaż wydaje mi się mało prawdopodobne, aby ludzie korzystali z indeksowanych darmowych monad na dwa różne sposoby w praktycznym kodzie.

{-# 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

Częściowe rozwiązanie. Możemy zdefiniować opakowanie typu, którego nie eksportujemy do konstruktora/akcesora.

To miałoby dwie funkcje prawie-ale-nie-całkiem-like-wiąże:

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) 

tylko w ten sposób klientów do tworzenia Caked wartości byłyby przez:

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

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

I byłoby przeznaczyć Cake wartości na callback:

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

To, myślę, zapewniłoby, że eat i keep zostaną wywołane tylko raz w ramach wywołania zwrotnego.

Problemy: nie działa z wieloma Cake alokacji i Cake wartości mogą nadal uciekać zakresu zwrotnego (Phantom typy mogłyby pomóc tutaj?)

Answer 3

Polakow pokazał w swoim referacie Haskell Sympozjum Embedding a full linear lambda calculus in Haskell (pdf), jak to zrobić.

Główną ideą jest indeksowanie każdego konstruktora za pomocą kontekstu wejściowego i wyjściowego śledzącego zasoby zużywane w różnych podteriach.