haskell - 如何从范围内的约束族派生类型类实例？

Question

编辑:我已经跟进了更多 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那是什么。 (编辑:我的真正问题涉及 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 的证明。 .
我敢肯定它比我想象的要简单。我尝试向 Object 添加约束 GADT 中的约束族类实例。我尝试在表达式的签名中提供约束。我试过 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))

Answer 1

如果没有更多上下文，很难说最好的解决方案是什么，但这里有几种可能性:
完全避免约束
就目前而言，您的 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 上递归.但这可能会变得非常繁琐。