編輯：我跟進了一個更具體的問題。感謝這里的回答者，我認為后續問題可以更好地解釋我在此處介紹的一些混淆。
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來自約束類別的類）
-- | 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))
uj5u.com熱心網友回復：
沒有更多的背景，很難說最好的解決方案是什么，但這里有幾種可能性：
完全避免約束
就目前而言，您的 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。但這可能會變得非常繁瑣。
uj5u.com熱心網友回復：
我認為正確的解決方案應該是這樣的：
-- 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)
轉載請註明出處，本文鏈接：https://www.uj5u.com/qukuanlian/365068.html
下一篇：以仆人和mtl風格流式傳輸