使受约束的函数成为类型类实例

Question

我对 Haskell 比较陌生，所以如果我的术语不完全正确，我深表歉意。

我正在尝试使用 Haskell 编写 Linear Temporal Logic 的实现，其中可以构造表达式，然后将其应用于元素列表以使用具有以下功能的函数生成布尔结果签名：

evaluate :: Expression a -> [a] -> Bool

Expression a 是代数数据类型，定义如下：

data Expression a = Conjunction (Expression a) (Expression a)
                  | Disjunction (Expression a) (Expression a)
                  | Next (Expression a)
                  | Always (Expression a)
                  | Eventually (Expression a)
                  | Until (Expression a) (Expression a)
                  | Predicate (a -> Bool)
                  -- etc. etc.

一切正常，但我想通过定义智能构造函数使构造表达式更优雅一些，理想情况下可以像这样使用：

numExpr :: Num a => Expression a
numExpr = eventually (== 10) `or` eventually (== 5)

到目前为止，我为实现这一目标所做的尝试包括以下内容：

eventually :: Expressable e => e a -> Expression a
eventually = Eventually . expresss

or :: (Expressable e, Expressable f) => e a -> f a -> Expression a
or x y = Or (express x) (express y)

-- and so on

class Expressable e where
  express :: e a -> Expression a

instance Expressable Expression where
  express = id

-- This is what I'd like to do:

type Pred a = a -> Bool

instance Expressable Pred where
  express = Predicate

但是后者不起作用。我试过使用各种 GHC 扩展（LiberalTypeSynonyms、TypeSynonymInstances），但似乎没有任何效果。这种事情是否可能，甚至是一个好主意？类型系统不允许这种事情有充分的理由吗？有没有更好的方法来构造它？

我知道我可以使用像 p :: (a -> Bool) -> Expression a 这样的签名的短函数名，但这仍然感觉有点不雅。

Answer 1

A newtype 而不是 type 会起作用：

newtype Pred a = Pred (a -> Bool)

instance Expressable Pred where
  express (Pred p) = Predicate p

在您的情况下，instance Expressable Pred where 中的 Pred 是部分应用的类型同义词，这些同义词基本上是不允许的（请参阅 LiberalTypeSynonyms 了解例外情况）。

Answer 2

在您的方法中，您需要 link a，即 Pred 的参数到 express 签名中的 a。这些必须相同，但您不能在 class / 实例中要求它们。

不过，您可以尝试这样的操作，并添加一系列扩展：

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

data Expression a = Conjunction (Expression a) (Expression a)
                  | Disjunction (Expression a) (Expression a)
                  | Next (Expression a)
                  | Always (Expression a)
                  | Eventually (Expression a)
                  | Until (Expression a) (Expression a)
                  | Predicate (a -> Bool)

class Expressable e a where
      express :: e -> Expression a
    
instance Expressable (Expression a) a where
  express = id

type Pred a = a -> Bool

instance Expressable (Pred a) a where
  express = Predicate

eventually :: Expressable e a => e -> Expression a
eventually = Eventually . express

or :: (Expressable e a, Expressable f a) => e -> f -> Expression a
or x y = Disjunction (express x) (express y)

我不太相信使用这种机制只是为了避免在原子公式上写 Predicate 是个好主意，但你可以试一试，看看它在实践中是否足够好.

使受约束的函数成为类型类实例

Make constrained functions a typeclass instance

haskell

typeclass