计算类型索引空闲monad的细节 [英] Working out the details of a type indexed free monad

问题描述

我一直在使用免费的monad构建DSL。作为该语言的一部分，有一个输入命令，目的是为了更加安全地反映输入原语在类型级别期望的类型。

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

  concat :: Action'[String，String]（）
 concat = do 
（x :: String）<  -  input 
（y :: String）<  -  input 
输出$ x ++++ y 
  

除了评估函数

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

/ p>

 > eval concat（a`HCons`b`HCons` HNil）
 [ab] 
  

$ p
$ b $ p $ lt; code> data HList i where
HNil :: HList'[ ]
HCons :: h - > HList t - > HList（h'：t）

类型append（a :: [k]）（b :: [k]）:: [k]其中
Append（'[]） l = l
Append（e'：l）l'= e'：（Append l'）

data ActionF next where
Input ::（a - >下一个） - > ActionF next
Output :: String - >下一个 - > ActionF next

实例Functor ActionF其中
fmap f（输入c）=输入（fmap fc）
fmap f（输出sn）=输出s（fn）

data FreeIx fia其中
Return :: a - > FreeIx f'[] a
Free :: f（FreeIx f i a） - > FreeIx f i a

类型Action a a = FreeIx ActionF i a

liftF :: Functor f => f a - > FreeIx f $ a
liftF =免费。 fmap返回

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（追加电视）b
bind（返回a）f = fa
bind（Free x）f = Free（fmap（flip bind f）x）

问题在于 liftF 不会输入check。

  liftF :: Functor f =>代理i  - > f a  - > FreeIx f i 
 liftF p =免费。 fmap返回
  

这是正确的做法吗？

我认为一些灵感可能来自效果monad 软件包。这导致了 Return 和 Free 的定义。

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

解决方案

我已经找到了一个令人满意的解决方案。这里有一个最终结果的偷看：

  addTwo = do 
（x :: Int）<  -  input 
（y :: Int）<  -  input 
 output $ show（x + y）
 
 eval（1 ::: 2 ::: HNil）addTwo = [ 3] 
  

完成此操作需要执行大量步骤。首先，我们需要注意到 ActionF 数据类型本身是索引的。我们将调整 FreeIx 来使用免费的monoid列表构建一个索引monad。 FreeIx 的 Free 构造函数将需要捕获证明其两个索引之一的有限性的证明以用于证明。我们将使用由于AndrásKovács撰写的关于附加类型级别列表的证明以进行证明结合性和正确的身份。我们将以与Oleg Grenrus 相同的方式描述索引monad 。我们将使用 RebindbableSyntax 扩展名为 IxMonad 使用普通的 do notation。

序言

除了您的示例所需的所有扩展外， 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 来操作类型相等。

  import Data.Type.Equality 
 import Data.Proxy 
  

因为我们将重新绑定 Monad 语法，我们将隐藏所有 Monad 来自 Prelude 导入。 RebindableSyntax 扩展名使用 do 表示法，无论函数>>> = ，>> 和失败在范围内。

b $ b

  import Prelude隐藏（Monad，（>> =），（>>），失败，返回）
  

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

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

I已将 Append 类型系列 ++ 重命名为镜像 ++
$ p $ type family（++）（a :: [k]）（b :: [k ]）:: [k]其中
'[] ++ l = l
（e'：l）++ l'= e'：l ++ l'


讨论形式 forall i的约束是有用的。 Functor（f i）。这些在GADT之外的 Haskell 中不存在，它们捕获 Dict 约束条件下的GADT 。就我们的目的而言，定义一个 Functor 的版本会有一个额外的被忽略的参数。

  class Functor1（f :: k  - > *  - > *）其中
 fmap1 ::（a  - > b） - > f i a  - > fib 
  





索引的ActionF

ActionF Functor 缺少一些东西，它无法捕获有关方法要求的类型级别信息。我们将添加一个额外的索引类型 i 来捕获它。 输入需要单一类型，'[a] ，而输出不需要任何类型，'[] 。

  data ActionF i next where 
输入： ：（a  - >下一个） - > ActionF'[a] next 
 Output :: String  - >下一个 - > ActionF'[] next 
  

我们会写 Functor 和 Functor1 < ActionF 。

<$ p $其中
fmap f（Input c）= Input（fmap fc）
fmap f（Output sn）= Output s（fn）

实例Functor1 ActionF其中
fmap1 f = fmap f

FreeIx Reconstructed

我们将对 FreeIx 进行两项更改。我们将改变索引的构建方式。 Free 构造函数将引用底层仿函数的索引，并产生一个 FreeIx ，其中索引是自由monoid来自底层仿函数的索引的总和（ ++ ）和被包装的 FreeIx 的索引。我们还要求 Free 捕获一个见证，以证明底层仿函数的索引是有限的。

  data FreeIx f（i :: [k]）a其中
 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 fi）其中
 fmap f（Return a）= Return（fa）
 fmap f（Free x）= Free（fmap1（fmap f）x）
 
 instance （Functor1 f）=> Functor1（FreeIx f）其中
 fmap1 f = fmap f 
  

如果我们要使用 FreeIx 与一个普通的，无索引的函子，我们可以将这些值提升到一个无约束的索引函数， IxIdentityT 。这是不需要这个答案。

  data IxIdentityT fia = IxIdentityT {runIxIdentityT :: fa} 
 
实例Functor f => Functor（IxIdentityT f i）其中
 fmap f = IxIdentityT。 fmap f。 runIxIdentityT 
 
实例Functor f => Functor1（IxIdentityT f）其中
 fmap1 f = fmap f 
  





证明

我们需要证明两个有关附加类型级别列表的属性。为了写 liftF ，我们需要证明正确的身份 xs ++'[]〜xs 。我们将这个证明称为 appRightId 来追加正确的身份。为了写 bind ，我们需要证明关联性 xs ++（yz ++ zs）〜（xs ++ ys）++ zs ，我们将称之为 appAssoc 。

证明以后继者list基本上是一个代理列表，每个类型一个 type SList xs〜HFMap Proxy（HList xs）。

  data SList（i :: [k]）其中
 SNil :: SList'[] 
 SSucc :: SList t  - > SList（h'：t）
  

下面的关联证明和写这个证明的方法是
由于AndrásKovács， 。通过对 xs 的类型列表仅使用 SList ，我们解构并使用 Proxy ys 需要 WitnessList 实例和 ZS 。

  appAssoc :: 
 SList xs  - >代理ys  - >代理zs  - > 
（xs ++（ys ++ zs））：〜：（（xs ++ ys）++ zs）
 appAssoc SNil ys zs = Refl 
 appAssoc（SSucc xs）ys zs = 
案例appAssoc xs ys zs of Refl  - > Refl 
  

Refl ，<$的构造函数c $ c>：〜：，只能在编译器拥有两种类型相等的证明时才能构造。 Refl 上的模式匹配将类型相等证明引入当前范围。

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

  appRightId :: SList xs  - > xs：〜：（xs ++'[]）
 appRightId SNil = Refl 
 appRightId（SSucc xs）= case appRightId xs Refl  - > Refl 
  

为了使用这些证明，我们构造了有限类列表类的证明列表。

  class WitnessList（xs :: [k]）其中
见证:: SList xs 
 
实例WitnessList'[]其中
 witness = SNil 
 
实例WitnessList xs => WitnessList（x'：xs）其中
 witness = SSucc证人
  

提升

配备 appRightId ，我们可以将底层仿函数的提升值定义为 FreeIx 。

  liftF :: forall f我a。 （WitnessList i，Functor1 f）=> f i a  - > FreeIx f i a 
 liftF = case的appRightId（见证:: SList i）Refl  - >自由 。 fmap1返回
  

显式 forall code> ScopedTypeVariables 。 Free 构造函数和<$ c $都需要索引有限性的见证 WitnessList i C> appRightId 。 appRightId 的证明用于说服编译器构造 FreeIx f（i ++'[]）a >与 FreeIx fia 类型相同。 '[] 来自包含在底层仿函数中的 Return 。

我们的两个命令 input 和输出，都是以 liftF 。

  type Action ia = FreeIx ActionF ia 
 
 input :: Action'[a] a 
 input = liftF（Input id）
 
 output :: String  - > Action'[]（）
 output s = liftF（Output s（））
  

IxMonad和绑定

要使用 RebindableSyntax ，我们将定义一个 IxMonad （>> =），（>>）， 失败为 Monad 但是不同的类型。 Oleg Grenrus的回答中描述了此类。

  class Functor1 m => IxMonad（m :: k  - > *  - > *）其中
类型Unit :: k 
类型Plus（i :: k）（j :: k）:: k 
 
 return :: a  - > m单位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  - > mia 
 fail s =错误s 
  

实现绑定 for FreeIx 需要关联证明， appAssoc 。范围内的 WitnessList 实例， WitnessList i ，是被解构的 Free 构造函数。显式 forall 用于 ScopedTypeVariables 。

  bind :: forall fija b。 （Functor1 f）=> FreeIx f i a  - > （a  - > FreeIx f j b） - > FreeIx f（i ++ j）b 
 bind（返回a）f = fa 
 bind（Free（x :: f i1（FreeIx f j1 a）））f = 
 case appAssoc （witness :: SList i1）（Proxy :: Proxy j1）（Proxy :: Proxy j）
 Refl  - > Free（fmap1（`bind` f）x）
  

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

  instance（Functor1 f）=> IxMonad（FreeIx f）其中
类型Unit ='[] 
类型Plus ij = i ++ j 
 
 return =返回
（>> =） = bind 
  

我们完成了

所有困难的部分都完成了。我们可以用最直接的方式为 Action xs（）编写一个简单的解释器。所需的唯一技巧是避免在 HList 构造函数 ::: 上的模式匹配，直到类型列表<$ c因为我们已经匹配 Input 。

，所以我们知道$ c> i 是非空的

  eval :: HList i  - >行动我（） - > [字符串] 
 eval输入操作= 
 
的操作返回（） - > [] 
空闲（输入f） - > 
案例输入
（x ::: xs） - > eval xs（f x）
 Free（下一个输出） - > s：eval input next 
  

如果您对 addTwo的推断类型感兴趣

  addTwo = do 
（x :: Int）<  -  input 
（y :: Int）<  -  input 
 output $ show（x + y）
  

它是

 > ：t addTwo 
 addTwo :: FreeIx ActionF'[Int，Int]（）
  

I've been using a free monad to build a DSL. As part of the language, there is an input command, the goal is to reflect what types are expected by the input primitive at the type level for additional safety.

For example, I want to be able to write the following program.

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

Along with an evaluation function

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

Which works in the following way..

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

Here's what I have so far.

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)

The problem is that liftF does not type check.

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

Is this the correct approach?

I thought some inspiration might come from the effect monad package. This is what led to the definition of Return and Free.

For some more backstory: I've seen in several places that users will define DSLs in this way and then define an evaluation function eval :: Action a -> [String] -> a or something similar. The clear problem with this approach is that all arguments must have the same type and there is no static guarantee that the correct number of arguments will be supplied. This is an attempt to solve this problem.

解决方案

I have found a satisfactory solution to this problem. Here's a sneak peek at the ultimate result:

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

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

Accomplishing this requires a large number of steps. First, we need to observe that the ActionF data type is itself indexed. We will adapt FreeIx to build an indexed monad using the free monoid, lists. The Free constructor for FreeIx will need to capture a witness to the finiteness of one of its two indexes for use in proofs. We will use a system due to András Kovács for writing proofs about appending type level lists to make proofs of both associativity and the right identity. We will describe indexed monads in the same manner as Oleg Grenrus. We will use the RebindbableSyntax extension to write expressions for an IxMonad using the ordinary do notation.

Prologue

In addition to all of the extensions your example already requires and RebindbableSyntax which was mentioned above we will also need UndecidableInstances for the trivial purpose of reusing a type family definition.

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

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

We will be using the :~: GADT from Data.Type.Equality to manipulate type equality.

import Data.Type.Equality
import Data.Proxy

Because we will be rebinding the Monad syntax, we'll hide all of Monad from the Prelude import. The RebindableSyntax extension uses for do notation whatever functions >>=, >>, and fail are in scope.

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

We also have a few bits of new general-purpose library code. I have given the HList an infix constructor, :::.

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

infixr 5 :::

I have renamed the Append type family ++ to mirror the ++ operator on lists.

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

It's useful to talk about constraints of the form forall i. Functor (f i). These don't exist in Haskell outside GADTs that capture constraints like the Dict GADT in constraints. For our purposes, it will be sufficient to define a version of Functor with an extra ignored argument.

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

Indexed ActionF

The ActionF Functor was missing something, it had no way to capture type level information about the requirements of the methods. We'll add an additional index type i to capture this. Input requires a single type, '[a], while Output requires no types, '[]. We are going to call this new type parameter the index of the functor.

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

We'll write Functor and Functor1 instances for 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 Reconstructed

We are going to make two changes to FreeIx. We will change how the indexes are constructed. The Free constructor will refer to the index from the underlying functor, and produce a FreeIx with an index that's the free monoidal sum (++) of the index from the underlying functor and the index from the wrapped FreeIx. We will also require that Free captures a witness to a proof that the index of the underlying functor is finite.

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

We can define Functor and Functor1 instances for 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

If we want to use FreeIx with an ordinary, unindexed functor, we can lift those values to an unconstrained indexed functor, IxIdentityT. This isn't needed for this answer.

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

We will need to prove two properties about appending type level lists. In order to write liftF we will need to prove the right identity xs ++ '[] ~ xs. We'll call this proof appRightId for append right identity. In order to write bind we will need to prove associativity xs ++ (yz ++ zs) ~ (xs ++ ys) ++ zs, which we will call appAssoc.

The proofs are written in terms of a successor list which is essentially a list of proxies, one for each type type SList xs ~ HFMap Proxy (HList xs).

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

The following proof of associativity along with the method of writing this proof are due to András Kovács. By only using SList for the type list of xs we deconstruct and using Proxys for the other type lists, we can delay (possibly indefinitely) needing WitnessList instances for 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, the constructor for :~:, can only be constructed when the compiler is in possession of a proof that the two types are equal. Pattern matching on Refl introduces the proof of type equality into the current scope.

We can prove the right identity in a similar fashion

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

To use these proofs we construct witness lists for the the class of finite type lists.

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

instance WitnessList '[] where
  witness = SNil

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

Lifting

Equipped with appRightId we can define lifting values from the underlying functor into 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

The explicit forall is for ScopedTypeVariables. The witness to the finiteness of the index, WitnessList i, is required by both the Free constructor and appRightId. The proof of appRightId is used to convince the compiler that the FreeIx f (i ++ '[]) a constructed is of the same type as FreeIx f i a. That '[] came from the Return that was wrapped in the underlying functor.

Our two commands, input and output, are written in terms of 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 and Binding

To use RebindableSyntax we'll define an IxMonad class with the same function names (>>=), (>>), and fail as Monad but different types. This class is described in 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

Implementing bind for FreeIx requires the proof of associativity, appAssoc. The only WitnessList instance in scope, WitnessList i, is the one captured by the deconstructed Free constructor. Once again, the explicit 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 is the only interesting part of the IxMonad instance for FreeIx.

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

    return = Return
    (>>=) = bind

We're done

All of the hard part is done. We can write a simple interpreter for Action xs () in the most straight forward fashion. The only trick required is to avoid pattern matching on the HList constructor ::: until after the type list i is known to be non-empty because we already matched on 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

If you are curious about the inferred type of addTwo

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

it is

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

这篇关于计算类型索引空闲monad的细节的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！