如何将 Haskell 中的约束含义编码为新的约束?在我的示例中,我想要求每个Functor c d f
需要都Obj c x
意味着Obj c (f x)
. 我正在写约束forall x . Obj c x => Obj d (f x)
。
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE QuantifiedConstraints #-}
import Prelude hiding (id, Functor, fmap)
import Data.Kind
class Category c where
type Obj c a :: Constraint
id :: (Obj c x) => c x x
comp :: (Obj c x) => c y z -> c x y -> c x z
class ( Category c, Category d, forall x . Obj c x => Obj d (f x))
=> Functor c d f where
fmap :: (Obj c x, Obj c y) => c x y -> d (f x) (f y)
doublefmap :: forall c f x . (Category c , Functor c c f, Obj c x)
=> c x x -> c (f (f x)) (f (f x))
doublefmap = fmap @c @c @f . fmap @c @c @f
但这会产生以下错误:
Minimal.hs:27:14: error:
• Could not deduce: Obj c (f x) arising from a use of ‘fmap’
from the context: (Functor c c f, Obj c x)
bound by the type signature for:
doublefmap :: forall (c :: * -> * -> *) (f :: * -> *) x.
(Category c, Functor c c f, Obj c x) =>
c x x -> c (f (f x)) (f (f x))
at Minimal.hs:(25,1)-(26,44)
• In the first argument of ‘(.)’, namely ‘fmap @c @c @f’
In the expression: fmap @c @c @f . fmap @c @c @f
In an equation for ‘doublefmap’:
doublefmap = fmap @c @c @f . fmap @c @c @f
• Relevant bindings include
doublefmap :: c x x -> c (f (f x)) (f (f x))
(bound at Minimal.hs:27:1)
我在这里做错了什么?我应该给编译器什么额外的提示?有没有更好的方法来实现这一点?
我的猜测是我需要使用Data.Constraint
and :-
,但是如何使用呢?