haskell - 计算类型索引的自由 monad 的细节

Question

我一直在使用免费的 monad 来构建 DSL。作为语言的一部分，有一个 input命令，目标是在类型级别反射(reflect)输入原语期望的类型，以提高安全性。

例如，我希望能够编写以下程序。

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

这是正确的方法吗？

我想一些灵感可能来自 effect 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使用自由的幺半群，列表来构建一个索引的 monad。 Free FreeIx 的构造函数将需要捕获其两个索引之一的有限性的见证以用于证明。我们将使用 system due to András Kovács for writing proofs about appending type level lists证明结合性和正确的身份。我们将 describe indexed monads in the same manner as Oleg Grenrus .我们将使用 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 #-}

我们将使用 :~: GADT from Data.Type.Equality 操纵类型相等。

import Data.Type.Equality
import Data.Proxy

因为我们将重新绑定(bind) 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) 的约束很有用.这些在 Haskell 中不存在在捕获约束的 GADT 之外，例如 the Dict GADT in constraints .就我们的目的而言，定义 Functor 的版本就足够了。带有额外的忽略参数。

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

索引 Action F
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索引是来自基础仿函数的索引和来自包装 ++ 的索引的自由幺半群和 ( 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)

以下结合性证明以及编写此证明的方法是
due to András Kovács .仅使用 SList对于 xs 的类型列表我们解构和使用 Proxy对于其他类型的列表，我们可以延迟(可能无限期地)需要 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 , Free 都需要构造函数和 appRightId . appRightId的证明用于说服编译器 FreeIx f (i ++ '[]) a构造的类型与 FreeIx 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 和绑定(bind)

使用 RebindableSyntax我们将定义一个 IxMonad具有相同函数名称的类 (>>=) , (>>) , 和 fail如 Monad但类型不同。此类在 Oleg Grenrus's answer 中有描述.

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] ()