时间戳

首页 > 解决方案 > GADT 的函子实例

haskell - GADT 的函子实例

问题描述

我正在尝试为 GADT 实现 Functor 实例，以试验 The Constrained-Monad Problem 论文。到目前为止，我的代码是这样的

{-# LANGUAGE GADTs #-}

data Expr a where
  I   :: Int -> Expr Int
  B   :: Bool -> Expr Bool
  Add :: Expr Int -> Expr Int->Expr Int
  Mul :: Expr Int -> Expr Int->Expr Int
  Eq  :: Eq a => Expr a -> Expr a -> Expr Bool

data ExprF a where
  Fmap :: (a->b) -> Expr a -> ExprF b

instance Functor ExprF where
  fmap f (Fmap g e) = Fmap (f . g ) e

liftExpr :: Expr a -> ExprF a
liftExpr = Fmap id

unliftExprF :: ExprF a-> Expr a
unliftExprF (Fmap f e) = e

eval :: Eq a => Expr a-> a
eval a =
  case a of
   I i -> i
   B b -> b
   Add a b -> eval a + eval b
   Mul a b -> eval a * eval b
   Eq a b -> (eval a) == (eval b)

eval2 :: Eq a => Expr a-> (a->b) -> b
eval2 a f = f $ eval a

class Reval a where
   reval :: a-> Expr a

instance Reval Int where
   reval i =  I i

instance Reval Bool where
   reval b = B b

类型是为了ExprF克服Eq约束。类型类Reval是为了Expr从一个值构造一个，因为我无法对原始类型（Int，Bool）进行模式匹配，我找不到更好的方法。liftExpr从. ExprF_ Expr问题是unliftExprF因为不进行类型检查。虽然对我来说这似乎是合乎逻辑的。上述论文讲述了 Functor 问题，但它使用了 ConstraintKinds。我也知道我可以使用 Rmonad 包，但我想自己尝试一下。任何帮助将不胜感激。谢谢。

标签： haskell

解决方案

在写下面的答案之前，我并没有真正仔细阅读您的代码。实际上，您设置它的方式似乎ExprF根本不需要任何特殊处理，因为这只是 a Coyoneda，即您强行将您的结构拉入Hask（或从概念上讲，Set）类别。因此，您的Functor实例工作得很好，但unliftExprF无法实现。但是，您可以忽略这一点并简单地使用

eval' :: ExprF a -> a
eval' (ExprF f x) = f $ eval x

原始答案

如果您的数据类型在逻辑上只能包含值，那么将其作为实例Eq是没有意义的。Prelude.Functor您也许可以使用额外的构造函数来解决这个问题，但这将是一团糟，并且会使数据类型几乎无法使用，因为您总是会遇到一个构造函数，该构造函数将实际结构隐藏在一个函数后面，该函数首先需要输入值可以做更多的事情。
（我应该知道，我已经多次涉足这样的 GADT。）

相反，您应该将自己限制在一个fmap对应于仅允许对该结构实际​​有意义的值的类别中，即基本上

class FunctorEq f where
  fmapEq :: (Eq a, Eq b) => (a -> b) -> f a -> f b

有许多课程可以满足这种一般需求。

  • 使用约束类：

    {-# LANGUAGE TypeFamilies #-}

import Control.ConstraintClasses

type instance Dom Expr a = Eq a

instance CFunctor Expr where
  _fmap = ...

  • 有约束的类别

    import qualified Prelude as Hask
import Control.Category.Constrained.Prelude

instance Functor Expr (Eq⊢(->)) (Eq⊢(->)) where
  fmap = ...

    然后你需要例如fmap (constrained (*2)) $ I 4`Add`I 5. （请注意，这是来自的$运算符Control.Arrow.Constrained。）

我建议使用constrained-categories，因为它不仅可以定义受约束类别中的函子，还可以定义更多类别理论概念，这些概念对于在 lambda 演算（如子语言）中生成表达式是必需的。但作为那个图书馆的作者，我有偏见......

推荐阅读