计算索引免费monad类型的详细信息

Question

我一直在使用免费的monad来构建DSL.作为语言的一部分,有一个input命令,目标是反映类型级别的输入原语所期望的类型,以增加安全性.

例如,我希望能够编写以下程序.

concat :: Action '[String, String] ()
concat = do
  (x :: String) <- input
  (y :: String) <- input 
  output $ x ++ " " ++ y

随着评估功能

eval :: Action params res -> HList params -> [String]
eval = ...

其中以下列方式工作..

> eval concat ("a" `HCons` "b" `HCons` HNil)
["a b"]

这是我到目前为止所拥有的.

data HList i where
  HNil :: HList '[]
  HCons :: h -> HList t -> HList (h ': t)

type family Append (a :: [k]) (b :: [k]) :: [k] where
  Append ('[]) l = l
  Append (e ': l) l' = e ': (Append l l')

data ActionF next where
   Input :: (a -> next) ->  ActionF next
   Output :: String -> next -> ActionF next

instance Functor ActionF where
  fmap f (Input c) = Input (fmap f c)
  fmap f (Output s n) = Output s (f n)

data FreeIx f i a where
  Return :: a -> FreeIx f '[] a
  Free :: f (FreeIx f i a) -> FreeIx f i a

type Action i a = FreeIx ActionF i a

liftF :: Functor f => f a -> FreeIx f i a
liftF = Free . fmap Return

input :: forall a . Action '[a] a
input = liftF (Input id)

output :: String -> Action '[] ()
output s = liftF (Output s ())

bind :: Functor f => FreeIx f t a -> (a -> FreeIx f v b) -> FreeIx f (Append t v) b
bind (Return a) f = f a
bind (Free x) f   = Free (fmap (flip bind f) x)

问题是liftF不进行类型检查.

liftF :: Functor f => Proxy i -> f a -> FreeIx f i a
liftF p = Free . fmap Return

这是正确的方法吗？

我认为一些灵感可能来自monad包的效果.这是什么导致的定义Return和Free.

对于更多的背景故事:我已经在几个地方看到用户将以这种方式定义DSL,然后定义评估函数eval :: Action a -> [String] -> a或类似的东西.这种方法的明显问题是所有参数必须具有相同的类型,并且没有静态保证将提供正确数量的参数.这是尝试解决这个问题.

Answer 1

我找到了一个令人满意的解决方案.这是对最终结果的预见:

addTwo = do
  (x :: Int) <- input
  (y :: Int) <- input 
  output $ show (x + y)

eval (1 ::: 2 ::: HNil) addTwo = ["3"]

实现这一点需要大量的步骤.首先,我们需要观察ActionF数据类型本身是否已编入索引.我们将FreeIx使用免费的monoid列表来适应构建索引monad.该Free用于构造FreeIx需要捕捉见证着两个指标用于证明使用一个的有限性.我们将使用AndrásKovács的系统来编写关于附加类型级别列表的证据,以证明关联性和正确的身份.我们将以与Oleg Grenrus相同的方式描述索引monad.我们将使用RebindbableSyntax扩展来IxMonad使用普通do表示法来编写表达式.

序幕

除了您的示例已经要求的所有扩展以及RebindbableSyntax上面提到的扩展之外,我们还需要UndecidableInstances重用类型系列定义的微不足道的目的.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RebindableSyntax #-}

我们将使用:~:GADTData.Type.Equality来操纵类型相等.

import Data.Type.Equality
import Data.Proxy

因为我们将重新绑定Monad语法,我们会隐藏所有的Monad来自Prelude进口.该RebindableSyntax扩展使用的do符号什么功能>>=,>>以及fail在范围.

import Prelude hiding (Monad, (>>=), (>>), fail, return)

我们还有一些新的通用库代码.我给了HList一个中缀构造函数,:::.

data HList i where
  HNil :: HList '[]
  (:::) :: h -> HList t -> HList (h ': t)

infixr 5 :::

我已重命名Append类型系列++以++在列表上镜像运算符.

type family (++) (a :: [k]) (b :: [k]) :: [k] where
  '[]      ++ l  = l
  (e ': l) ++ l' = e ': l ++ l'

谈论表单的约束是有用的forall i. Functor (f i).这些在HaskellGADT中不存在,它们在约束中捕获像GADT这样的Dict约束.出于我们的目的,定义Functor具有额外忽略参数的版本就足够了.

class Functor1 (f :: k -> * -> *) where
    fmap1 :: (a -> b) -> f i a -> f i b

索引ActionF

在ActionF Functor失去了一些东西,它没有办法捕捉有关方法的需求类型级别的信息.我们将添加一个额外的索引类型i来捕获它.Input需要单一类型,'[a]而不Output需要任何类型,'[].我们将这个新类型参数称为仿函数的索引.

data ActionF i next where
   Input :: (a -> next) ->  ActionF '[a] next
   Output :: String -> next -> ActionF '[] next 

我们会写Functor和Functor1实例ActionF.

instance Functor (ActionF i) where
  fmap f (Input c) = Input (fmap f c)
  fmap f (Output s n) = Output s (f n)

instance Functor1 ActionF where
  fmap1 f = fmap f

FreeIx重建

我们将进行两项修改FreeIx.我们将改变索引的构造方式.该Free构造将参照索引从底层函子,并产生一个FreeIx与这就是自由monoidal总和(索引++从底层函子索引,并从包裹的索引)FreeIx.我们也会要求Free捕获证据,证明底层函子的索引是有限的.

data FreeIx f (i :: [k]) a where
  Return :: a -> FreeIx f '[] a
  Free :: (WitnessList i) => f i (FreeIx f j a) -> FreeIx f (i ++ j) a

我们可以定义Functor和Functor1实例FreeIx.

instance (Functor1 f) => Functor (FreeIx f i) where
  fmap f (Return a) = Return (f a)
  fmap f (Free x) = Free (fmap1 (fmap f) x)

instance (Functor1 f) => Functor1 (FreeIx f) where
  fmap1 f = fmap f

如果我们想要使用FreeIx普通的无索引函子,我们可以将这些值提升为无约束的索引函子,IxIdentityT.这个答案不需要这个.

data IxIdentityT f i a = IxIdentityT {runIxIdentityT :: f a}

instance Functor f => Functor (IxIdentityT f i) where
    fmap f = IxIdentityT . fmap f . runIxIdentityT

instance Functor f => Functor1 (IxIdentityT f) where
    fmap1 f = fmap f

证明

我们需要证明有关附加类型级别列表的两个属性.为了写,liftF我们需要证明正确的身份xs ++ '[] ~ xs.我们将此声明称为appRightId附加权身份.为了写,bind我们需要证明关联性xs ++ (yz ++ zs) ~ (xs ++ ys) ++ zs,我们将称之为appAssoc.

证明是根据后继列表编写的,后者列表基本上是代理列表,每种类型一个 type SList xs ~ HFMap Proxy (HList xs).

data SList (i :: [k]) where
  SNil :: SList '[]
  SSucc :: SList t -> SList (h ': t)

关联与写这个证明的方法大致如下证明是 由于安德拉斯·科瓦克斯.通过仅使用我们解构SList的类型列表xs并将Proxys用于其他类型列表,我们可以延迟(可能无限期地)需要WitnessList实例ys和zs.

appAssoc ::
  SList xs -> Proxy ys -> Proxy zs ->
  (xs ++ (ys ++ zs)) :~: ((xs ++ ys) ++ zs)
appAssoc SNil ys zs = Refl
appAssoc (SSucc xs) ys zs =
  case appAssoc xs ys zs of Refl -> Refl

Refl,构造函数:~:只能在编译器拥有两种类型相等的证明时构造.模式匹配Refl将类型相等的证明引入当前范围.

我们可以以类似的方式证明正确的身份

appRightId :: SList xs -> xs :~: (xs ++ '[])
appRightId SNil = Refl
appRightId (SSucc xs) = case appRightId xs of Refl -> Refl

为了使用这些证明,我们为有限类型列表的类构建见证列表.

class WitnessList (xs :: [k]) where
  witness :: SList xs

instance WitnessList '[] where
  witness = SNil

instance WitnessList xs => WitnessList (x ': xs) where
  witness = SSucc witness

吊装

配备appRightId我们可以从底层仿函数定义提升值FreeIx.

liftF :: forall f i a . (WitnessList i, Functor1 f) => f i a -> FreeIx f i a
liftF = case appRightId (witness :: SList i) of Refl -> Free . fmap1 Return

明确的forall是ScopedTypeVariables.构造函数和构造函数WitnessList i都需要见证索引的有限性.证明用于说服编译器构造的类型与.那来自于底层仿函数.FreeappRightIdappRightIdFreeIx f (i ++ '[]) aFreeIx f i a'[]Return

我们两个命令,input并output都写在条款liftF.

type Action i a = FreeIx ActionF i a

input :: Action '[a] a
input = liftF (Input id)

output :: String -> Action '[] ()
output s = liftF (Output s ())

IxMonad和Binding

要使用RebindableSyntax我们定义的IxMonad具有相同功能的名称类(>>=),(>>)和fail作为Monad,但不同的类型.Oleg Grenrus的回答描述了这一课程.

class Functor1 m => IxMonad (m :: k -> * -> *) where
    type Unit :: k
    type Plus (i :: k) (j :: k) :: k

    return :: a -> m Unit a
    (>>=) :: m i a -> (a -> m j b) -> m (Plus i j) b

    (>>) :: m i a -> m j b -> m (Plus i j) b
    a >> b = a >>= const b

    fail :: String -> m i a
    fail s = error s

实施bind为FreeIx需要关联的证据,appAssoc.WitnessList范围中唯一的实例WitnessList i是解构Free构造函数捕获的实例.再一次,明确的forall是ScopedTypeVariables.

bind :: forall f i j a b. (Functor1 f) => FreeIx f i a -> (a -> FreeIx f j b) -> FreeIx f (i ++ j) b
bind (Return a) f = f a
bind (Free (x :: f i1 (FreeIx f j1 a))) f =
    case appAssoc (witness :: SList i1) (Proxy :: Proxy j1) (Proxy :: Proxy j)
    of Refl -> Free (fmap1 (`bind` f) x)

bind是IxMonad实例中唯一有趣的部分FreeIx.

instance (Functor1 f) => IxMonad (FreeIx f) where
    type Unit = '[]
    type Plus i j = i ++ j

    return = Return
    (>>=) = bind

我们完成了

所有困难的部分都完成了.我们可以用Action xs ()最直接的方式编写一个简单的解释器.唯一需要的技巧是避免HList构造函数上的模式匹配,:::直到i知道类型列表非空为止,因为我们已经匹配Input.

eval :: HList i -> Action i () -> [String]
eval inputs action = 
    case action of 
        Return () -> []
        Free (Input f) -> 
            case inputs of
                (x ::: xs) -> eval xs (f x)
        Free (Output s next) -> s : eval inputs next

如果你对推断的类型感到好奇 addTwo

addTwo = do
  (x :: Int) <- input
  (y :: Int) <- input 
  output $ show (x + y)

它是

> :t addTwo
addTwo :: FreeIx ActionF '[Int, Int] ()

Answer 2

我有一个简单且非常普遍适用的新解决方案.

到目前为止,在线程中我们使用了由monoid索引的monad,但是在这里我依赖于索引monad的另一个流行概念,即具有typestate过渡的那个(Hoare逻辑风格):

    return :: a -> m i i a
    (>>=) :: m i j a -> (a -> m j k b) -> m i k b

我相信这两种方法是等价的(至少在理论上),因为我们通过使用内同态monoid索引来获得Hoare monad,并且我们也可以通过CPS编码状态转换中的monoidal附加来反向.在实践中,Haskell的类型级和类级语言相当弱,因此在两个表示之间来回移动不是一种选择.

但是上述类型存在一个问题>>=:它意味着我们必须以自上而下的顺序计算类型状态,即它强制执行以下定义IxFree:

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

所以,如果我们有一个Free exp表达式,那么我们首先从过渡i到j下面的构造函数exp,然后从获得j到k通过检查的subexperssions exp.这意味着如果我们尝试input在列表中累积类型,我们最终会得到一个反向列表:

-- compute transitions top-down
test = do
  (x :: Int) <- input       -- prepend Int to typestate
  (y :: String) <- input    -- prepend String to typestate
  return ()                 -- do nothing         

如果我们将类型附加到列表的末尾,则顺序是正确的.但是eval,如果有可能,那么在Haskell(尤其是制作工作)中进行这项工作就需要大量的校对.

让我们自下而上计算类型状态.它使得我们根据语法树建立一些数据结构的各种计算更加自然,特别是它使我们的工作变得非常容易.

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

import Prelude hiding (Monad(..))

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

class IxFunctor m => IxMonad (m :: ix -> ix -> * -> *) where
    return :: a -> m i i a
    (>>=) :: m j k a -> (a -> m i j b) -> m i k b -- note the change of index orders

    (>>) :: m j k a -> m i j b -> m i k b -- here too
    a >> b = a >>= const b

    fail :: String -> m i j a
    fail = error

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

instance IxFunctor f => Functor (IxFree f i j) where
  fmap f (Pure a)  = Pure (f a)
  fmap f (Free fa) = Free (imap (fmap f) fa)

instance IxFunctor f => IxFunctor (IxFree f) where
  imap = fmap

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

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

现在实施Action变得简单.

data ActionF i j next where
  Input  :: (a -> next) -> ActionF i (a ': i) next
  Output :: String -> next -> ActionF i i next

deriving instance Functor (ActionF i j)                                      
instance IxFunctor ActionF where
  imap = fmap

type family (++) xs ys where -- I use (++) here only for the type synonyms
  '[] ++ ys = ys
  (x ': xs) ++ ys = x ': (xs ++ ys)

type Action' xs rest = IxFree ActionF rest (xs ++ rest)
type Action xs a = forall rest. IxFree ActionF rest (xs ++ rest) a  

input :: Action '[a] a
input = liftf (Input id)

output :: String -> Action '[] ()
output s = liftf (Output s ())

data HList i where
  HNil :: HList '[]
  (:::) :: h -> HList t -> HList (h ': t)
infixr 5 :::

eval :: Action' xs r a -> HList xs -> [String]
eval (Pure a)              xs         = []
eval (Free (Input k))      (x ::: xs) = eval (k x) xs
eval (Free (Output s nxt)) xs         = s : eval nxt xs

addTwice :: Action [Int, Int] ()
addTwice = do
  x <- input
  y <- input
  output (show $ x + y)

为了减少对用户的混淆,我引入了带有友好索引方案的类型同义词:Action' xs rest a意味着该操作从xs包含rest读取的操作读取并可能跟随.Action是一个类型同义词,等同于线程问题中出现的同义词.

我们可以用这种方法实现各种DSL.反向打字顺序给它一点旋转,但我们可以做通常的索引monad所有相同.这是索引状态monad,例如:

data IxStateF i j next where
  Put :: j -> next -> IxStateF j i next
  Get :: (i -> next) -> IxStateF i i next

deriving instance Functor (IxStateF i j)
instance IxFunctor IxStateF where imap = fmap

put s = liftf (Put s ())
get   = liftf (Get id)

type IxState i j = IxFree IxStateF j i

evalState :: IxState i o a -> i -> (a, o)
evalState (Pure a)         i = (a, i)
evalState (Free (Get k))   i = evalState (k i) i
evalState (Free (Put s k)) i = evalState k s

test :: IxState Int String ()
test = do
  n <- get
  put (show $ n * 100)

现在,我相信这种方法比使用monoids进行索引更实用,因为Haskell没有类型类或第一类类型级函数可以使幺半群方法变得可口.有一个VerifiedMonoid类,比如in Idris或者Agda,包括正常方法之外的正确性证明,这将是很好的.这样我们就可以FreeIx在索引monoid的选择中编写一个通用的,而不仅限于提升列表或其他内容.

Answer 3

关于索引monad的简短说明:它们是由monoids索引的monad.比较默认monad:

class Monad m where
  return :: a -> m a
  bind :: m a -> (a -> m b) -> m b
  -- or `bind` alternatives:
  fmap :: (a -> b) -> m a -> m b
  join :: m (m a) -> m a

monoid是一种配有mempty- identity元素和(<>) :: a -> a -> a二元关联操作的类型.提升到类型级别我们可以有Unit类型和Plus关联二进制类型操作.注意,列表是值级别上的免费monoid,并且HList是类型级别.

现在我们可以定义索引的monoid类:

class IxMonad m where
  type Unit
  type Plus i j

  return :: a -> m Unit a
  bind :: m i a -> (a -> m j b) -> m (Plus i j) b
  --
  fmap :: (a -> b) -> m i a -> m i b
  join :: m i (m j a) -> m (Plus i j) a

您可以为索引版本说明monad法律.您会注意到,对于要对齐的索引,它们必须遵守幺半群定律.

随着免费单子你要装备一个Functor与return和join操作.稍微改变你的定义是有效的:

data FreeIx f i a where
  Return :: a -> FreeIx f '[] a -- monoid laws imply we should have `[] as index here!
  Free :: f (FreeIx f k a) -> FreeIx f k a

bind :: Functor f => FreeIx f i a -> (a -> FreeIx f j b) -> FreeIx f (Append i j) b
bind (Return a) f = f a
bind (Free x) f   = Free (fmap (flip bind f) x)

我不得不承认,我不是百分之百确定Free构造函数索引是如何合理的,但它们似乎有效.如果我们考虑功能wrap :: f (m a) -> m a的MonadFree具有法律类:

wrap (fmap f x) ? wrap (fmap return x) >>= f

和有关评论Free中free包

在实践中,您可以只查看包含类型值的Free f多个层,其中执行替换并为每个自由变量移植新的in 层.fa(>>=)f

那么这个想法是包装值不会影响索引.

但是,您希望将任意f值提升为任意索引的monadic值.这是一个非常合理的要求.但唯一有效的定义强制提升价值'[]- Unit或mempty指数:

liftF :: Functor f => f a -> FreeIx f '[] a
liftF = Free . fmap Return

如果您尝试将Return定义更改为:: a -> FreeIx f k a(k,不是[]- 纯值可能具有任意索引),则bind定义将不会键入check.

我不确定你是否可以使免费的索引monad仅使用小的修正.一个想法是将任意monad提升为索引monad:

data FreeIx m i a where
  FreeIx :: m a -> FreeIx m k a

liftF :: Proxy i -> f a -> FreeIx f i a
liftF _ = FreeIx

returnIx :: Monad m => a -> FreeIx m i a
returnIx = FreeIx . return

bind :: Monad m => FreeIx m i a -> (a -> FreeIx m j b) -> FreeIx m (Append i j) b
bind (FreeIx x) f = FreeIx $ x >>= (\x' -> case f x' of
                                             FreeIx y -> y)

这种方法有点像作弊,因为我们总是可以重新索引价值.

另一种方法是提醒 Functor它是一个索引的仿函数,或者像Cirdec的答案那样立即使用索引仿函数开始.

Answer 4

如果您愿意牺牲隐式排序并使用显式访问器,则Action '[Int, Int]可以使用ReaderT (HList '[Int, Int]).如果您使用像vinyl镜头一样的现有库,您可以编写如下内容:

-- Implemented with pseudo-vinyl
-- X and Y are Int fields, with accessors xField and yField
addTwo :: ReaderT (PlainRec '[X, Y]) Output ()
addTwo = do
  x <- view (rGet xField)
  y <- view (rGet yField)
  lift . output $ show (x + y) -- output :: String -> Output ()

类型安全由约束传播强制执行:rGet xField引入作为X记录成员的要求.

对于没有类型级机械的简单说明,请比较:

addTwo :: ReaderT (Int, Int) IO ()
addTwo = do
  x <- view _1
  y <- view _2
  lift . putStrLn $ show (x + y)

我们失去了排序属性,这是一个重大的损失,特别是如果排序是有意义的,例如代表用户交互的顺序.

此外,我们现在必须使用runReaderT(〜eval).我们不能说,用户输入与输出交错.