我正在定義一個型別引數有一些關系的型別。我有使用and的Item型別，但是你可以使用一些依賴于的型別。例如，當您指定as時，您可以指定or as 。CatSubCatSubCatCatCat1CatSubCat1SubCat2SubCat

我使用 type family 來實作它來為 eachValidSubCats定義有效的 s ，并使用type family 來定義一個約束。SubCatCatOneOf

{-# LANGUAGE DataKinds, GADTs, PolyKinds, StandaloneKindSignatures, TypeFamilies, TypeOperators #-}

import Data.Kind (Constraint, Type)
import Data.Type.Equality ((:~:)(..), TestEquality(..))
import Unsafe.Coerce (unsafeCoerce)

data Cat = Cat1 | Cat2
type SCat :: Cat -> Type
data SCat cat where
    SCat1 :: SCat 'Cat1
    SCat2 :: SCat 'Cat2

data SubCat = SubCat1 | SubCat2 | SubCat3
type SSubCat :: SubCat -> Type
data SSubCat subCat where
    SSubCat1 :: SSubCat 'SubCat1
    SSubCat2 :: SSubCat 'SubCat2
    SSubCat3 :: SSubCat 'SubCat3

type ValidSubCats :: Cat -> [SubCat]
type family ValidSubCats cat where
    ValidSubCats 'Cat1 = '[ 'SubCat1, 'SubCat2 ]
    ValidSubCats 'Cat2 = '[ 'SubCat2, 'SubCat3 ]

type OneOf :: k -> [k] -> Constraint
type family OneOf t ts where
    OneOf t (t ': _) = ()
    OneOf t (_ ': ts) = OneOf t ts
    OneOf _ _ = ('True ~ 'False)

type Item :: Cat -> SubCat -> Type
data Item cat subCat where
    Item :: OneOf subCat (ValidSubCats cat) => Item cat subCat

現在，我正在嘗試定義一個函式來創建Itemfrom SCatand SSubCat。

type HL :: (k -> Type) -> [k] -> Type
data HL f t where
    HCons :: f t -> HL f ts -> HL f (t ': ts)
    HNil :: HL f '[]
infixr 5 `HCons`

validSSubCats :: SCat cat -> HL SSubCat (ValidSubCats cat)
validSSubCats SCat1 = SSubCat1 `HCons` SSubCat2 `HCons` HNil
validSSubCats SCat2 = SSubCat2 `HCons` SSubCat3 `HCons` HNil

instance TestEquality SSubCat where
    testEquality SSubCat1 SSubCat1 = Just Refl
    testEquality SSubCat2 SSubCat2 = Just Refl
    testEquality SSubCat3 SSubCat3 = Just Refl
    testEquality _ _ = Nothing

oneOf :: TestEquality f => f t -> HL f ts -> Maybe (OneOf t ts :~: (() :: Constraint))
oneOf x (HCons y ys) = case testEquality x y of
                           Just Refl -> Just Refl
                           Nothing -> unsafeCoerce $ oneOf x ys
oneOf _ HNil = Nothing

makeItem :: SCat cat -> SSubCat subCat -> Maybe (Item cat subCat)
makeItem sCat sSubCat = case oneOf sSubCat (validSSubCats sCat) of
                            Just Refl -> Just Item
                            Nothing -> Nothing

但正如你所看到的，我正在使用unsafeCoerce來定義oneOf. 當我洗掉它時，我得到了這個錯誤。

test.hs:54:39: error:
    ? Could not deduce: OneOf t ts1 ~ OneOf t (t1 : ts1)
      from the context: ts ~ (t1 : ts1)
        bound by a pattern with constructor:
                   HCons :: forall {k} (f :: k -> *) (t :: k) (ts :: [k]).
                            f t -> HL f ts -> HL f (t : ts),
                 in an equation for ‘oneOf’
        at q.hs:52:10-19
      Expected: Maybe (OneOf t ts :~: (() :: Constraint))
        Actual: Maybe (OneOf t ts1 :~: (() :: Constraint))
      NB: ‘OneOf’ is a non-injective type family
    ? In the expression: oneOf x ys
      In a case alternative: Nothing -> oneOf x ys
      In the expression:
        case testEquality x y of
          Just Refl -> Just Refl
          Nothing -> oneOf x ys
    ? Relevant bindings include
        ys :: HL f ts1 (bound at q.hs:52:18)
        y :: f t1 (bound at q.hs:52:16)
        x :: f t (bound at q.hs:52:7)
        oneOf :: f t
                 -> HL f ts -> Maybe (OneOf t ts :~: (() :: Constraint))
          (bound at q.hs:52:1)
   |
54 |                            Nothing -> oneOf x ys
   |                                       ^^^^^^^^^^

我怎樣才能說服 GHC 它可以OneOf t (t ': ts) :~: (() :: Constraint)在OneOf t ts :~: (() :: Constraint)不使用的情況下進行推斷unsafeCoerce？

uj5u.com熱心網友回復：

我建議使用具有價值級別表示的東西，因為我們可以更輕松地直接操作這些東西。一般來說，這通常更容易使用。例如：

data OneOf' t ts where
  Here :: forall t ts. OneOf' t (t ': ts)
  There :: forall t t2 ts. OneOf' t ts -> OneOf' t (t2 ': ts)

oneOf' :: TestEquality f => f t -> HL f ts -> Maybe (OneOf' t ts)
oneOf' _ HNil = Nothing
oneOf' x (HCons y ys) =
  case testEquality x y of
    Just Refl -> Just Here
    Nothing -> There <$> oneOf' x ys

這并沒有直接回答所問的問題，盡管如果您可以撰寫一個帶有 type 的函式

convertOneOf :: forall t ts. OneOf' t ts -> (OneOf t ts :~: (() :: Constraint))

那么它將回答確切的問題。現在，我不確定如何做到這一點（甚至是否可能）。我認為您需要一個輔助功能

weakenOneOf :: forall t t2 ts. OneOfTrue t ts -> OneOfTrue t (t2 ': ts)

（我使用同義詞OneOfTrue使事情更容易閱讀：）type OneOfTrue t ts = OneOf t ts :~: (() :: Constraint)。

如果這可以實作，那么你應該很高興，盡管我可能仍然希望盡可能使用OneOf'。

值得注意的是，likeOneOf'是依賴型別語言中相對常見的構造：這里有一個 Agda 示例，這里有一個 Idris 示例，這里有一個 Coq 中的類似內容。它們中的每一個都以相同的方式具有價值級別的內容OneOf'。

Item可以重寫為OneOf'這樣使用：

type Item' :: Cat -> SubCat -> Type
data Item' cat subCat where
    Item' :: OneOf' subCat (ValidSubCats cat) -> Item' cat subCat

并且有一個相應的重寫供makeItem使用Item'。

為什么原版OneOf很棘手并且OneOf'不那么棘手

通常很難使用類似OneOf. 原因之一是 Haskell 允許型別族“卡住”。這可以防止某些型別級別的“減少”，并且我們沒有規范形式之類的東西。

例如，考慮這個定義，它在處理傳遞給 a 的型別級串列時可能很有用OneOf：

listDecideNilCons :: forall ts. Either (ts :~: '[]) (IsCons ts)
listDecideNilCons = ...

data IsCons a where
  MkIsCons :: forall t ts. IsCons (t ': ts)

listDecideNilCons只會告訴您型別級串列是 nil 或 cons，這看起來很合理，并且可以方便地使用。事實上，我懷疑有必要能夠實作listDecideNilCons或類似的東西才能實作convertOneOf. 我更強烈地懷疑有必要實作另一個方向的轉換。

但是，卡住型別族的存在足以說明listDecideNilCons無法實作。考慮：

type family Sticky (b :: Bool) :: [Int] where
  Sticky True = '[]

example :: Either ((Sticky False) :~: '[]) (IsCons (Sticky False))
example = listDecideNilCons

此代碼型別檢查。的值應該example是多少？由于Sticky False無法進一步減少，因此沒有任何example意義。

請注意，如果我們也有值級別的資訊，就像我們對 所做的那樣OneOf'，我們不會遇到這個問題，原因有兩個： 卡住的型別不是問題，因為我們可以控制允許我們使用哪些特定的“形狀”（如'[]和）... ': ...當我們構建新事物的證明時，我們可以使用證明值。

例如，在 的情況下OneOf'，它確保型別級串列將具有“形狀” ... ': ...。在函式oneOf'中，我們使用來自遞回呼叫的證明值oneOf' x ys來構建更大的證明。

在原始oneOf函式中，我們不能利用遞回呼叫的結果將具有“cons 形狀”或回傳Nothing（因為原始OneOf函式沒有給我們此資訊）這一事實。但是，我們必須知道這一點才能使用遞回呼叫的結果來產生所需的結果，因為原始呼叫OneOf 需要“cons 形狀”。

標籤：哈斯克尔 类型级计算 单例型

上一篇：簡化太長的Haskell函式

下一篇：HaskellmapM_不列印