edit:我接着提出了一个更具体的问题。谢谢这里的回答者,我认为后续问题更好地解释了我在这里介绍的一些困惑。
<小时 />里拉;DR我正在努力将约束证明放入表达式中,同时在构造函数上使用具有存在约束的 GADT。(这是严重的拗口,对不起!
我已将问题提炼为以下几点。我有一个简单的 GADT,它表示称为X
的点和称为F
的函数应用程序。X
的点被约束为Objects
。
data GADT ix a where
X :: Object ix a => a -> GADT ix a
F :: (a -> b) -> GADT ix a -> GADT ix b
Constrained
是指其对象受某物约束的容器,Object
是某物。(编辑:我真正的问题涉及约束类别的Category
和Cartesian
类)
-- | I can constrain the values within containers of kind `* -> *`
class Constrained (ix :: * -> *) where
type Object ix a :: Constraint
-- | Here's a trivial constraint. A more interesting one might include `Typeable a`, for ex
instance Constrained (GADT ix) where
type Object (GADT ix) a = (Constrained ix, Object ix a)
我想写一个表达式:
-- error: Could not deduce: Object ix Int arising from a use of ‘X’
ex0 :: GADT ix String
ex0 = F show (X (3 :: Int))
虽然显而易见的解决方案有效,但在构建更大的表达式时,它很快就会变得冗长:
-- Typechecks, but eventually verbose
ex1 :: Object ix Int => GADT ix String
ex1 = F show (X (3 :: Int))
我认为正确的解决方案应该是这样的:
-- error: Could not deduce: Object ix Int arising from a use of ‘X’
ex2 :: Constrained ix => GADT ix String
ex2 = F show (X (3 :: Int))
但我仍然无法获得Object ix Int
的证据.
我相信这比我想象的要简单。我尝试在GADT
类实例中向Object
约束系列添加约束。我尝试在表达式的签名中提供约束。我已经尝试过QuantifiedConstraints
,虽然,我不确定我是否完全掌握了它。请帮助我聪明的人!
可运行:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE InstanceSigs #-}
module Test where
import Data.Kind
import Data.Functor.Identity
import Data.Functor.Const
-- | I can constrain the values within containers of kind `* -> *`
class Constrained (ix :: * -> *) where
type Object ix a :: Constraint
-- | Here's a trivial constraint. A more interesting one might include `Typeable a`, for instance
instance Constrained (GADT ix) where
type Object (GADT ix) a = (Constrained ix, Object ix a)
-- | A demo GADT that has function application ('F'), and points ('X'). The
-- points are constrained.
data GADT ix a where
X :: Object ix a => a -> GADT ix a
F :: (a -> b) -> GADT ix a -> GADT ix b
-- -- Broken
-- -- error: Could not deduce: Object ix Int arising from a use of ‘X’
-- ex0 :: GADT ix String
-- ex0 = F show (X (3 :: Int))
-- Typechecks
-- but for larger programs becomes verbose, requiring many explicit constraints
ex1 :: Object ix Int => GADT ix String
ex1 = F show (X (3 :: Int))
-- -- What I want, but, it's broken
-- ex2 :: Constrained ix => GADT ix String
-- ex2 = F show (X (3 :: Int))
如果没有更多的上下文,很难说什么是最好的解决方案,但这里有几种可能性:
完全避免约束
就目前而言,您的 GADT 似乎没有太多理由将X
限制为Object
。也许这只是不需要的?
data GADT ix a where
X :: a -> GADT ix a
F :: (a -> b) -> GADT ix a -> GADT ix b
相反,在需要时,约束可能来自外部。
咬住约束列表的项目符号,但使它们更好
如果表达式中有许多不同类型的类型都需要满足相同的约束,则可以使用类似All
ex2' :: All (Object ix) '[Int] => GADT ix String
ex2' = F show (X (3 :: Int))
除了Int
之外,列表中还可以有更多类型;和/或您可以创建同义词约束,例如
type StdObjs ix = (Object ix Int, Object x Bool, ...)
ex2'' :: StdObjs ix => GADT ix String
ex2'' = F show (X (3 :: Int))
通过数据结构本身向后传播约束
如果您确实需要对X
值进行约束,仍然可以在 GADT 中以另一种方式表达这一点。例如,如果函数不是通用函数,而是已经约束为只接受Object
s 的函数,则可以这样使用它:
data YourFunc ix a b where
YourFunc :: Object ix a => (a->b) -> YourFunc ix a b
show' :: Object ix Int => YourFunc ix Int String
show' = YourFunc show
这并不能直接帮助您解决所询问的问题,但也许该功能是共享的或其他什么。你甚至可以有类似的东西
class Object ix a => InferrenceChain ix a where
type PreElem ix a :: Type
propInferrence :: (InferrenceChain ix (PreElem a) => r) -> r
然后
data YourFunc ix a b where
YourFunc :: InferrenceChain ix a
=> (PreElem a -> a) -> YourFunc (PreElem a) a
然后最后,你可以证明X
约束,只需在外部放入Object ix String
并在propInferrence
上递归。但这可能会变得相当繁琐。
我认为正确的解决方案应该是这样的:
-- error: Could not deduce: Object ix Int >arising from a use of ‘X’ ex2 :: Constrained ix => GADT ix String ex2 = F show (X 3)
不幸的是,这个解决方案没有任何意义。编译器有理由指出它不知道Object ix Int
此时是否满意,因为它所知道的是Constrained ix
可能会通过Object ix Int
施加一些约束。
通过量化的解决方案
因此,也许你想要的是一个约束,它说:"在这一点上,我使用的所有Object ix a
约束都得到了满足"——我们可以尝试通过量化来做到这一点:
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ConstraintKinds #-}
type Satisfied ix = forall a. Object ix a
ex2 :: Satisfied ix => GADT ix String
ex2 = F show (X 3)
不幸的是,这给了我们一个GHC错误:
• Quantified predicate must have a class or type variable head:
forall a. Object ix a
• In the quantified constraint ‘forall a. Object ix a’
In the type synonym declaration for ‘Satisfied’
由于Object
是一个类型族,而不是类或类型变量。
重新架构
但。。。为什么Object
是一个类型家族?事实上,Constrained
为什么会作为一个没有方法的无法无天的阶级存在呢?如果我们想对容器和类型的组合施加约束,Haskell已经为我们提供了做到这一点的方法 - 只需使用实例约束!
{-# LANGUAGE MultiParamTypeClasses #-}
class Object ix a
type Constrained ix = forall a. Object ix a
因为如果我们有
instance (...<some stuff>...) => Constrained Foo where
type Object ix a = (...<some def>...)
我们可以将其翻译为
instance (...<some stuff>..., ...<some def>...)
=> Object ix a
这使得此示例可以编译。
ex2 :: Constrained ix => GADT ix String
ex2 :: F show (X 3)