Есть ли способ подражать линейным типам в Haskell?

Я моделирую систему, в которой есть операция, которая создает ресурс и другие операции, которые потребляют этот ресурс. Однако данный ресурс можно использовать только один раз - есть ли способ, которым я могу гарантировать, что во время компиляции?

Для конкретности, скажем, первая операция выпекает торт и что есть еще две операции: одна для "выбора еды" торта, а другая для "выбора пирога" и что я могу сделать только один или другие.

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

Его легко обеспечить соблюдение ограничения не хранить уже съеденный торт (или наоборот) во время выполнения, установив флаг на торт после его использования. Но есть ли способ обеспечить это во время компиляции?

Кстати, этот вопрос предназначен для доказательства концепции, поэтому я в порядке с любой черной магией, которая может дать мне статическую безопасность, которую я хочу.

Ответ 1

В Haskell базовая версия этого может быть выражена с помощью GADT, индексированного хранилищем тортов (представленным списком 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 ()

К сожалению, мы не можем удалить аннотации типа из действий Bake и оставить типы для вывода:

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

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

Очевидно, что (Elem (New cs0) (New cs0 + 1 : New cs0 : cs0)) является выполнимым для всех cs0, но GHC не может этого видеть, потому что он не может решить, является ли New cs0 неравенством New cs0 + 1, поскольку GHC не может ничего принять в отношении гибкого cs0.

Если мы добавим NoMonomorphismRestriction, foo будет typecheck, но это сделает даже неправильные программы typecheck, нажав все ограничения Elem на верх. Тем не менее это все равно помешает делать что-нибудь полезное с неправильными терминами, но это довольно уродливое решение.

В более общем плане мы можем выразить Bake как индексированную свободную монаду, которая получает do -notation с RebindableSyntax и позволяет определение для BakeF несколько яснее, чем мы видели раньше, Он также может уменьшить шаблон, похожий на обычную старую монаду Free, хотя я считаю маловероятным, что люди могли бы использовать для индексированных свободных монад в двух разных случаях в практическом коде.

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

Ответ 2

Полаков показал в своей статье симпозиума Haskell Внедрение полного линейного лямбда-исчисления в Haskell (pdf), как это сделать.

Основная идея состоит в том, чтобы индексировать каждый конструктор с помощью входного и выходного контекстов, отслеживающих ресурсы, потребляемые в разных субтермах.

Ответ 3

Частичное решение. Мы можем определить тип оболочки

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

из которого мы не экспортируем конструктор /accessor.

У него было бы две функции почти-но-совсем-как-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)

Единственный способ для клиентов создавать значения Caked - это:

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

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

И мы бы выделили значения Cake для обратного вызова:

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

Это, я думаю, обеспечит, чтобы eat и keep вызывались только один раз в обратном вызове.

Проблемы: не работает с несколькими распределениями Cake, а значения Cake все еще могут выходить из области обратного вызова (может ли помощь здесь phantom)?