具有型別級別Bool的GADT-使(&&)型別運算子暗示對其引數的約束

總之，我試圖了解如何在 GADT 的背景關系中告訴ghc 這a && b ~ True應該暗示這一點。a ~ Trueb ~ True

給定一個資料建構式：

data Foo :: Bool -> * where
    ...
    Bar :: Foo j -> Foo k -> Foo (j && k)
    ...

并且，作為一個例子，一個實體Eq (Foo True)：

instance Eq (Foo True) where
   (Bar foo11 foo12) == (Bar foo21 foo22) = foo11 == ff21 && foo12 == foo22
   ....

編譯器給出以下錯誤：

Could not deduce: k1 ~ k
      from the context: 'True ~ (j && k)
        bound by a pattern with constructor:
                   Bar :: forall (j :: Bool) (k :: Bool).
                          Foo j -> Foo k -> Foo (j && k),
                 in an equation for `=='
        at Main.hs:12:4-14
      or from: 'True ~ (j1 && k1)
        bound by a pattern with constructor:
                   Bar :: forall (j :: Bool) (k :: Bool).
                          Foo j -> Foo k -> Foo (j && k),
                 in an equation for `=='
        at Main.hs:12:21-31
      `k1' is a rigid type variable bound by
        a pattern with constructor:
          Bar :: forall (j :: Bool) (k :: Bool).
                 Foo j -> Foo k -> Foo (j && k),
        in an equation for `=='
        at Main.hs:12:21-31
      `k' is a rigid type variable bound by
        a pattern with constructor:
          Bar :: forall (j :: Bool) (k :: Bool).
                 Foo j -> Foo k -> Foo (j && k),
        in an equation for `=='
        at Main.hs:12:4-14
      Expected type: Foo k
        Actual type: Foo k1
    * In the second argument of `(==)', namely `f22'
      In the second argument of `(&&)', namely `f12 == f22'
      In the expression: f11 == f21 && f12 == f22
    * Relevant bindings include
        f22 :: Foo k1 (bound at Main.hs:12:29)
        f12 :: Foo k (bound at Main.hs:12:12)

（以及 j 和 j1 的等效錯誤）

這顯然是在抱怨它不知道f12 :: Foo k并且f22 :: Foo k1具有相同的型別。

最近我一直在使用 typelit-nat-normalise 來解決感覺類似的問題（添加 typenat），并且我已經搜索了一個類似的庫，可以解決這些布爾問題 - 但無濟于事。

我找到了 typelevel-rewrite-rules，我認為這可能使我能夠為此撰寫某種重寫規則，但我無法找出告訴編譯器的語法：

(a && b ~ True)暗示(a ~ True) AND (b ~ True)。我相信這會解決這個問題。

uj5u.com熱心網友回復：

我相信在當前的 GHC 中，這種型別族的“反轉”是不可能的，至少在沒有不安全功能的情況下是不可能的。

即使有不安全的功能，我也不知道添加它是否安全。種類是奇怪的野獸，并且通常包含比預期更多的術語。例如type family X :: Bool編譯，我們仍然無法證明X ~ 'Truenor X ~ 'False。

下面的代碼并沒有完全回答這個問題，但我想說的是，如果我們可以添加一些約束Foo來攜帶一些單例，那么我們可以撰寫想要的Eq實體。

下面的代碼可能可以進一步簡化。盡管如此，它還是在這里。下面，我定義了“轉換”函式fooT1, fooT2來讓 GHC 相信我們確實Foo k有.Foo jk ~ j ~ 'True

{-# LANGUAGE GADTs, ScopedTypeVariables, TypeApplications,
    DataKinds, TypeOperators, KindSignatures,
    FlexibleInstances, AllowAmbiguousTypes #-}
{-# OPTIONS -Wall #-}

import Data.Singletons
import Data.Singletons.Prelude.Bool

data Foo :: Bool -> * where
    Bar :: (SingI j, SingI k) =>
           Foo j -> Foo k -> Foo (j && k)

fooT1 :: forall a b. (SingI a, SingI b, (a && b) ~ 'True) 
      => Foo a -> Foo b -> Foo 'True
fooT1 f _ = case (sing @a, sing @b) of
   (STrue, STrue) -> f

fooT2 :: forall a b. (SingI a, SingI b, (a && b) ~ 'True)
      => Foo a -> Foo b -> Foo 'True
fooT2 _ f = case (sing @a, sing @b) of
   (STrue, STrue) -> f

instance Eq (Foo 'True) where
   (Bar foo11 foo12) == (Bar foo21 foo22) = 
      fooT1 foo11 foo12 == fooT1 foo21 foo22 &&
      fooT2 foo11 foo12 == fooT2 foo21 foo22

請注意，模式匹配(STrue, STrue)是詳盡的，GHC 不會發出任何警告。

標籤：哈斯克尔 ghc 类型检查

上一篇：如何在串列中獲取多個第n個元素？

下一篇：我可以在將字串切割成頭部和尾部（a：as）并在Haskell中對其使用遞回之后將其用作整個字串嗎？