haskell - Sigma 中的限制类型

Question

我有类型 X按种类索引 S具有适用于 X 的几个功能.例如，f转换 X S1至 X S2 (不过，在这个简化的例子中它不使用 X S1)。

{-# LANGUAGE DataKinds, GADTs, TemplateHaskell, TypeFamilies #-}

import Data.Singletons
import Data.Singletons.Sigma
import Data.Singletons.TH

singletons [d|
    data S = S1 | S2 | S3 | S4
  |]

data X (s :: S) = X

f :: X S1 -> X S2
f x = X

现在我想定义可能返回 X S2 的函数或 X S3取决于它的论点。直接的方法是使用 Either .

g1 :: Bool -> X S1 -> Either (X S2) (X S3)
g1 True x = Left X
g1 False x = Right X

但我不想采用这种方法，因为我需要嵌套 Either s 当函数返回更多类型时。
另一种方法是使用 Sigma像这样。

g2 :: Bool -> X S1 -> Sigma S (TyCon X)
g2 True x = SS2 :&: X
g2 False x = SS3 :&: X

但这并没有表达 g2 的想法仅返回 X S2或 X S3 .我可以通过在 X 周围引入一个包装器来表达这个想法。 .

data Y (s :: S) where
    Y2 :: X S2 -> Y S2
    Y3 :: X S3 -> Y S3

singletons [d|
    type Z s = Y s
  |]

g3 :: Bool -> X S1 -> Sigma S ZSym0
g3 True x = SS2 :&: Y2 X
g3 False x = SS3 :&: Y3 X

但是为每个组合定义这些包装器并在调用者站点上打开它们是很麻烦的。如果我可以使用 g2 直接限制类型就好了方法，例如，通过喜欢应用类型约束，但我不知道我该怎么做。
如何使用 g2 直接限制类型方法？
我正在使用 GHC 8.8.4 和 singletons-2.6 .

Answer 1

这个问题看起来过于简单和做作；有一些更具体的动机会很好。但这是黑暗中的一个镜头。
我们可以定义 Sigma 的变体在第一个组件上使用谓词:

data SigmaP (i :: Type) (p :: i ~> Constraint) (f :: i -> Type) where
  (:&?:) :: (p @@ x) => Sing x -> f x -> SigmaP i p f

一些定义谓词的代码似乎是不可避免的:

data Y23 :: S ~> Constraint
type instance Apply Y23 x = Y23_ x

type family Y23_ (x :: S) :: Constraint where
  Y23_ S2 = (() :: Constraint)
  Y23_ S3 = (() :: Constraint)
  Y23_ _ = ('True ~ 'False)

但是现在我们可以使用 X :

g3 :: Bool -> X S1 -> SigmaP S Y23 X
g3 True x = SS2 :&?: X
g3 False x = SS3 :&?: X