时间戳

首页 > 解决方案 > 限制 Sigma 中的类型

haskell - 限制 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当函数返回更多类型时，我需要嵌套 s。

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

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

但这并不表示g2只返回X S2or的想法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一起使用。

标签： haskelldependent-typesingleton-type

解决方案

这个问题看起来太简单和做作了；有一些更具体的动机会很好。但这是在黑暗中拍摄的。

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

推荐阅读