simbolos - if en haskell ejemplos

¿Hay una manera de emular tipos lineales en Haskell?

Question

Estoy modelando un sistema que tiene una operación que crea un recurso y otras operaciones que consumen ese recurso. Sin embargo, un recurso determinado solo se puede consumir una vez. ¿Hay alguna forma de garantizarlo en el momento de la compilación?

Para concretar, digamos que la primera operación hace una torta y que hay otras dos operaciones, una para "elegir comer" la torta y otra para "elegir tener la torta" y que solo puedo hacer una o la otra.

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

Es fácil hacer cumplir la restricción de no mantener un pastel ya comido (o viceversa) en el tiempo de ejecución al colocar una bandera en el pastel después de que lo usemos. ¿Pero hay una manera de hacer cumplir esto en tiempo de compilación?

Por cierto, esta pregunta es para una prueba de concepto, así que estoy de acuerdo con cualquier magia negra que pueda brindarme la seguridad estática que quiero.

Answer 1

En Haskell, una versión básica de esto podría expresarse con un GADT indexado por una tienda de pasteles (representada por una lista de Nat ):

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

Desafortunadamente, no podemos eliminar las anotaciones de tipo de las acciones de Bake y dejar que se infieran los tipos:

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

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

Obviamente, (Elem (New cs0) (New cs0 + 1 : New cs0 : cs0)) es satisfactorio para todos los cs0 , pero GHC no puede ver esto, porque no puede decidir si New cs0 es desigual al New cs0 + 1 , porque GHC no puede asumir nada sobre la variable cs0 flexible.

Si agregamos NoMonomorphismRestriction , foo haría una verificación de tipo, pero eso haría que incluso los programas incorrectos se verifiquen al colocar todas las restricciones Elem en la parte superior. Sin embargo, esto todavía evitaría hacer algo útil con términos incorrectos, pero es una solución bastante fea.

De manera más general, podemos expresar Bake como una mónada libre indexada, lo que nos permite do anotación con RebindableSyntax , y permite una definición de BakeF que es algo más clara de lo que hemos visto antes. También podría reducir la repetición al igual que la antigua mónada Free simple, aunque me parece bastante improbable que la gente encuentre uso para las mónadas indexadas libres en dos ocasiones diferentes en el código práctico.

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

Polakow mostró en su papel de Haskell Symposium Incrustar un cálculo lambda lineal completo en Haskell (pdf) sobre cómo hacerlo.

La idea principal es indexar cada constructor con una entrada y un contexto de salida que haga un seguimiento de los recursos consumidos en los diversos subterms.

Answer 3

Una solución parcial. Podríamos definir un tipo de envoltura

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

de los cuales no exportamos el constructor / accesor.

Tendría dos funciones casi vinculantes, pero no del todo parecidas:

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)

La única forma en que los clientes pueden crear valores Caked sería a través de:

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

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

Y asignaríamos los valores de Cake en una devolución de llamada:

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

Esto, creo, aseguraría que eat y keep solo sean llamados una vez dentro de la devolución de llamada.

Problemas: no funciona con múltiples asignaciones de Cake y los valores de Cake todavía pueden escapar al alcance de la devolución de llamada (¿podrían ayudar los tipos fantasma aquí?)