限制 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

现在我想根据参数定义 return X S2 或 X S3 的函数。直接的方法是使用 Either.

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

但我不想采用这种方法，因为当一个函数 returns 更多类型时，我需要嵌套 Eithers。

另一种方法是像这样使用 Sigma。

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

但这并没有表达 g2 return 只有 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 方法直接限制类型？

我在 singletons-2.6.

中使用 GHC 8.8.4

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

Answer 2

受 . It's similar to 启发的另一种方法，但使用明确的类型列表。

{-# LANGUAGE DataKinds, GADTs, EmptyCase, InstanceSigs, PolyKinds, ScopedTypeVariables, TemplateHaskell, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-}

import Data.Kind
import Data.Singletons
import Data.Singletons.Prelude
import Data.Singletons.TH

singletons [d|
    data S = S1 | S2 | S3 | S4 deriving (Show, Eq)
  |]

data X (s :: S) = X

data SigmaL (l :: [s :: Type]) (t :: s ~> Type) where
    (:&!:) :: OneOf fst l => Sing (fst :: s) -> t @@ fst -> SigmaL l t

type family OneOf s l :: Constraint where
    OneOf s l = If (Elem s l) (() :: Constraint) ('True ~ 'False)

g5 :: Bool -> X S1 -> SigmaL '[S2, S3] (TyCon X)
g5 True x = SS2 :&!: X
g5 False x = SS3 :&!: X

限制 Sigma 中的类型

Restrict types in Sigma

haskell

dependent-type

singleton-type