Gibt es eine Möglichkeit, lineare Typen in Haskell zu emulieren?

Question

Ich modelliere ein System mit einer Operation, die eine Ressource und andere Operationen erstellt, die diese Ressource verbrauchen. Eine bestimmte Ressource kann jedoch nur einmal verwendet werden - gibt es eine Möglichkeit, die ich zur Kompilierzeit garantieren kann?

Für Konkretheit, sagen wir, die erste Operation backt einen Kuchen und es gibt zwei andere Operationen, eine für "Wählen, um den Kuchen zu essen" und eine für "den Kuchen zu wählen" und dass ich nur einen machen kann das andere.

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

Die leicht eine Einschränkung des nicht halten, einen bereits gegessen Kuchen (oder umgekehrt) zur Laufzeit erzwingen, indem sie einen Flag auf dem Kuchen nach Einstellung wir sie verwenden. Aber gibt es eine Möglichkeit, dies zur Kompilierzeit durchzusetzen?

BTW, diese Frage ist für einen Proof of Concept gedacht, also bin ich OK mit jeder schwarzen Magie, die mir die statische Sicherheit geben kann, die ich will.

Answer 1

In Haskell, eine Basisversion von diesem mit einem GADT durch einen Shop von Kuchen (durch eine Liste von Nat -s dargestellt) indiziert ausgedrückt werden könnte:

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

Leider ist der Typ nicht entfernen können wir Anmerkungen aus Bake Aktionen und lassen Typen abgeleitet werden:

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

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

Offensichtlich (Elem (New cs0) (New cs0 + 1 : New cs0 : cs0)) erfüllbar ist dies für alle cs0, aber GHC kann nicht sehen, weil es nicht darum, obentscheiden können,ist ungleich New cs0 + 1, weil GHC nichts über die flexible cs0 Variable annehmen kann.

Wenn wir NoMonomorphismRestriction hinzufügen, würde foo typecheck, aber das würde sogar falsche Programme typecheck machen, indem Sie alle Elem Einschränkungen an die Spitze schieben. Dies würde zwar immer noch verhindern, dass etwas Nützliches mit falschen Begriffen gemacht wird, aber es ist eine ziemlich hässliche Lösung.

---

Allgemeiner können wir Bake als indiziertes frei Monade ausdrücken, die uns do -Notation mit RebindableSyntax wird, und ermöglicht eine Definition für BakeF, die etwas klarer ist als das, was wir bisher gesehen haben. Es könnte auch Boilerplate viel wie die einfache alte Free Monade reduzieren, obwohl ich es eher unwahrscheinlich finde, dass Leute Gebrauch für indizierte freie Monaden zu zwei verschiedenen Gelegenheiten im praktischen Code finden würden.

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

Eine Teillösung. Wir könnten einen Wrappertyp definieren

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

von denen wir den Konstruktor/Accessor nicht exportieren.

Es zwei fast-but-not-quite-like-bind Funktionen haben würde:

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) 

Die einzige Möglichkeit für die Kunden Caked Werte zu schaffen wäre durch:

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

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

Und wir Cake Werte auf einen Rückruf zuweisen würde:

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

Dies würde, denke ich, sicherstellen, dass eat und keep nur einmal innerhalb des Callbacks aufgerufen werden.

Probleme: funktionieren nicht mit mehrer Cake Zuweisungen und Cake Werte können immer noch den Umfang des Rückrufs entkommen (könnten Arten Phantom helfen hier?)

Answer 3

Polakow in seinem Haskell Symposium Papier zeigte Embedding a full linear lambda calculus in Haskell (pdf), wie dies zu tun.

Die Hauptidee besteht darin, jeden Konstruktor mit einem Eingabe- und Ausgabekontext zu indizieren, der die in den verschiedenen Unterkategorien verwendeten Ressourcen verfolgt.