0

我正在编码（作为假设）函子恒等律，如下所示：

...
import qualified Prelude ()
...


{-@ class Functor f where
      fmap :: forall a b. (a -> b) -> (f a -> f b) @-}
class Functor f where
  fmap :: (a -> b) -> (f a -> f b)


-- identity function
{-@ id :: forall a . x : a -> {y : a | x = y} @-}
id :: forall a . a -> a
id x = x

-- functor law: mapping with identity is identity
{-@ assume
    fmap_id :: forall f a . Functor f => x : f a ->
      {fmap id x = id x} @-}
fmap_id :: Functor f => f a -> ()
fmap_id _ = ()

我看不出这个公式有什么问题，但是我从 LH 那里得到了这个错误：

src/Category/Functor/LH.hs:45:16: error:
    • Illegal type specification for `Category.Functor.LH.fmap_id`
    Category.Functor.LH.fmap_id :: forall f a .
                                   (Functor<[]> f) =>
                                   x:f a -> {VV : () | Category.Functor.LH.fmap Category.Functor.LH.id x == Category.Functor.LH.id x}
    Sort Error in Refinement: {VV : Tuple | Category.Functor.LH.fmap Category.Functor.LH.id x == Category.Functor.LH.id x}
    Unbound symbol Category.Functor.LH.fmap --- perhaps you meant: Category.Functor.LH.C:Functor ?
    •
   |
45 |     fmap_id :: forall f a . Functor f => x : f a ->
   |

我究竟做错了什么？我的目标是用可扩展性来表述这个无点，但至少这个逐点表述应该首先起作用。

配置：

  • GHC 版本：8.10.1
  • 阴谋集团版本：3.2.0.0
  • Liquid Haskell 版本：0.8.10.2
4

1 回答 1

1

Liquid Haskell 的官方版本尚不支持对类型类的支持（尽管它几乎已准备好合并）。现在，你可以使用这个实现类型类支持的fork 。递归克隆存储库后，您可以使用以下命令安装分叉版本：

pushd liquid-benchmark/liquidhaskell
stack install
popd

我们定义Functor及其定律（在VFunctor子类中）liquid-base/liquid-base/src/Data/Functor/Classes.hs如下。请注意，您可以直接在类型类方法上指定细化。

class Functor f where
  {-@ fmap :: forall a b. (a -> b) -> f a -> f b @-}
  fmap :: (a -> b) -> f a -> f b
  (<$) :: a -> f b -> f a

class Functor m => VFunctor m where
  {-@ lawFunctorId :: forall a . x:m a -> {fmap id x == id x} @-}
    lawFunctorId :: m a -> ()

  {-@ lawFunctorComposition :: forall a b c . f:(b -> c) -> g:(a -> b) -> x:m a -> { fmap (compose f g) x == compose (fmap f) (fmap g) x } @-}
  lawFunctorComposition :: forall a b c. (b -> c) -> (a -> b) -> m a -> ()

您可以使用以下命令在类型类定义上运行分叉版本的 Liquid Haskell：

liquid --typeclass -i liquid-base/liquid-base/src/ liquid-base/liquid-base/src/Data/Functor/Classes.hs

我们创建一个经过验证的Maybe实例liquid-base/liquid-base/src/Data/Maybe/Functor.hs：

instance Functor Maybe where
  fmap _ Nothing = Nothing
  fmap f (Just x) = Just (f x)
  _ <$ Nothing = Nothing
  x <$ (Just _) = Just x

instance VFunctor Maybe where
  lawFunctorId Nothing = ()
  lawFunctorId (Just _) = ()
  lawFunctorComposition f g Nothing = ()
  lawFunctorComposition f g (Just x) = ()

您可以在实例上运行 Liquid HaskellMaybe以验证它是否满足所需的法律：

liquid --typeclass -i liquid-base/liquid-base/src/ liquid-base/liquid-base/src/Data/Maybe/Functor.hs
于 2020-12-28T15:30:32.743 回答