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

我一直在使用免费的 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

这是正确的方法吗？

我想一些灵感可能来自于效应单子 https://hackage.haskell.org/package/effect-monad包裹。这就是导致定义的原因Return and Free.

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

我已经找到了解决这个问题的满意方法。以下是最终结果的预览：

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

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

实现这一点需要大量步骤。首先，我们需要观察到ActionF数据类型本身是索引的。我们会适应FreeIx使用免费的 monoid、lists 构建索引 monad。这Free构造函数FreeIx将需要捕获其两个索引之一的有限性的证据以用于证明。我们将使用一个感谢 András Kovács 的系统，用于编写有关附加类型级别列表的证明 https://gist.github.com/AndrasKovacs/c45c0e005013dc468c76证明关联性和正确的身份。我们将以与 Oleg Grenrus 相同的方式描述索引单子 https://stackoverflow.com/a/27678650/414413。我们将使用RebindbableSyntax扩展来编写表达式IxMonad使用普通的do符号。

Prologue

除了您的示例已经需要的所有扩展之外，RebindbableSyntax上面提到的我们还需要UndecidableInstances为了重用类型族定义的简单目的。

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

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

我们将使用:~:GADT 来自Data.Type.Equality http://hackage.haskell.org/package/base-4.7.0.2/docs/Data-Type-Equality.html操纵类型相等。

import Data.Type.Equality
import Data.Proxy

因为我们将重新绑定Monad语法，我们将隐藏所有Monad来自Prelude进口。这RebindableSyntax扩展用于do任何功能的符号>>=, >>, and 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 https://hackage.haskell.org/package/constraints-0.4.1.1/docs/Data-Constraint.html。出于我们的目的，定义一个版本就足够了Functor带有额外的被忽略的参数。

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

索引动作F

The ActionF Functor缺少一些东西，它无法捕获有关方法要求的类型级别信息。我们将添加一个额外的索引类型i捕捉这一点。Input需要单一类型，'[a], while Output不需要类型，'[]。我们将这个新类型参数称为函子的索引。

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

我们会写Functor and 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 and 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

Proofs

我们需要证明关于附加类型级别列表的两个属性。为了写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)

以下结合性证明以及编写该证明的方法是由于安德拉斯·科瓦奇 https://gist.github.com/AndrasKovacs/c45c0e005013dc468c76。仅通过使用SList对于类型列表xs我们解构并使用Proxy对于其他类型列表，我们可以延迟（可能无限期地）需要WitnessList的实例ys and 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

Lifting

配备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 is for ScopedTypeVariables。证明该指数的有限性，WitnessList i，两者都需要Free构造函数和appRightId。的证明appRightId用于让编译器相信FreeIx f (i ++ '[]) a构造的类型与FreeIx f i a. That '[]来自Return它被包裹在底层函子中。

我们的两个命令，input and 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 和绑定

To use RebindableSyntax我们将定义一个IxMonad具有相同函数名的类(>>=), (>>), and fail as Monad但类型不同。这个类的描述在奥列格·格伦鲁斯的回答 https://stackoverflow.com/a/27678650/414413.

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 for FreeIx需要关联性证明，appAssoc。唯一的WitnessList范围内的实例，WitnessList i，是被解构捕获的Free构造函数。再次明确forall is for 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)

it is

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