限制Sigma中的类型

如何解决限制Sigma中的类型

我有一个类型为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。

另一种方法是像这样使用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方法直接限制类型？

我在singletons-2.6上使用GHC 8.8.4。

解决方法

这个问题看起来过于简化和人为。有一些更具体的动机会很好。但这是黑暗中的一枪。

我们可以定义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

另一种受@luqui's comment启发的方法。它类似于@li-yao-xia's answer，但使用了明确的类型列表。

{-# 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