如何从作用域中的约束族派生类型类实例？ [英] How can I derive typeclass instances from constraint families that are in scope?

问题描述

编辑：我已经跟进了更多specific question。感谢这里的答题者，我认为接下来的问题更好地解释了我在这里介绍的一些念力。

---

tl；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是某物约束的容器。(edit：我的实际问题涉及Category和Cartesian来自constrained-categories的类)

-- | 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中用另一种方式来表达。例如，如果函数不是，而是已经被约束为只接受Objects的函数，则它可以是这样的：

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上递归。但这可能会相当麻烦。

这篇关于如何从作用域中的约束族派生类型类实例？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！