时间戳

首页 > 解决方案 > 使用 Bound 与多个类型变量进行抽象

haskell - 使用 Bound 与多个类型变量进行抽象

问题描述

我一直在尝试绑定包 - 您可以尝试使用的一个玩具示例是 System F。与包文档中的示例不同，这些示例具有一个用于被 lambda 绑定的变量的类型参数，System F 将有两个类型参数，一种用于普通变量（受普通 lambda 抽象约束），另一种用于类型变量（受类型抽象约束）。

我不太明白如何使用该包，但查看示例，我得到的印象是我应该从编写Monad表达式类型的实例开始。但是，我遇到了麻烦，因为我无法提出可以进行类型检查并且“显然正确”的东西（即通过检查看起来直观正确）。到目前为止我有

{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE LambdaCase #-}

module SystemF where

import Bound
import Control.Monad
import Data.Bifunctor

-- e ::= x | λx : τ. e | e1 e2 | ΛX. e | e [τ]
-- t denotes type variables, e denotes expression variables
data Exp t e
  = Var e
  | Lam (Scope () (Exp t) e)
  | App (Exp t e) (Exp t e)
  | TyLam (Scope () (FlipExp e) t) -- Is this correct?
  | TyApp (Exp t e) (Type t)

newtype FlipExp e t = FlipExp { getExp :: Exp t e }

instance Functor (Exp t) where
  fmap = second

instance Bifunctor Exp where
  bimap f g = \case
    Var e -> Var (g e)
    Lam s -> Lam (bimapInScope f g s)
    App e1 e2 -> App (bimap f g e1) (bimap f g e2)
    TyLam s' -> TyLam (bimapInScope g f s')
    TyApp e t -> TyApp (bimap f g e) (fmap f t)
    where
      bimapInScope f g = Scope . bimap f (second (bimap f g)) . unscope

instance Applicative (Exp t) where
  pure = Var
  (<*>) = ap

instance Monad (Exp t) where
  x >>= f = case x of
    Var v -> f v
    Lam s -> Lam (s >>>= f)
    App e1 e2 -> App (e1 >>= f) (e2 >>= f)
    TyLam s ->
      -- tmp :: Exp (Var () (Exp t a) a
      -- but we need Exp (Var () (Exp t b)) b
      -- just applying >>= inside the first argument 
      -- is insufficient as the outer 'a' won't change
      let tmp = first (second getExp) $ getExp (unscope s)
      in error "How do I implement this?"
    TyApp e t -> TyApp (e >>= f) t

instance Functor (FlipExp e) where
  fmap = second

instance Bifunctor FlipExp where
  bimap f g = FlipExp . bimap g f . getExp

-- τ ::= X | τ -> τ | ∀ X . τ
data Type t
  = TVar t
  | TFun (Type t) (Type t)
  | TForall (Scope () Type t)
  deriving (Functor, Foldable, Traversable)

instance Applicative Type where
  pure = TVar
  (<*>) = ap

instance Monad Type where
  x >>= f = case x of
    TVar v -> f v
    TFun t1 t2 -> TFun (t1 >>= f) (t2 >>= f)
    TForall s -> TForall (s >>>= f)
  1. 是否有可能有一个单子实例Exp t？如果是，如何？
  2. Monad 实例背后的直觉是什么？对于 State/Maybe monad，我发现将它们视为链接计算（就绑定而言）很有用，而对于像列表这样的结构，我发现从扁平化的角度考虑（就连接而言）很有用）。但是，我无法为 Exp 的 Monad 实例提供任何适当的直觉。bind 是否精确地进行了避免捕获的替换？我通读了这篇文章，但在普通的“De Bruijn 指数”部分之后迷路了。

标签： haskellmonads

解决方案

请参阅此处的讨论和此处的@phadejbound-extras包。

要点是类型抽象是一个术语级别的东西（因此是 的变体Expr），需要对Types 进行抽象。PlainScope b f a不适合处理这个问题，因为它的扩展f (Either b (f a))对于f这两种情况都是固定的。您希望外部f是 a Expr，而内部应该是 a Type。这导致以下概括Scope：

newtype ScopeH b f g a = ScopeH (g (Either b (f a)))
newtype ScopeT b t f a = ScopeT (t f (Either b (f a)))

newtype Expr' a b = Expr' (Expr b a)
data Expr b a
  = V a
  ...
  | TyApp (Expr b a) (Ty b)
  | Forall (ScopeH () (Expr' a) Ty b)
  ...

Expr' a修复了术语 vars 的 de Bruijn 索引，以便ScopeH构造函数可以引入额外的类型 var 以放入b孔中。

推荐阅读