Ограничить типы в 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?

Я использую GHC 8.8.4 с singletons-2.6.


singleton-type haskell dependent-type
person snak    schedule 01.10.2020    source источник
comment
Как насчет использования списка типов g :: Bool -> X S1 -> OneOf '[X S2, X S3] для подходящего определения OneOf?   -  person luqui    schedule 01.10.2020
comment
@luqui Спасибо. Я попробую написать это, но я был бы признателен, если бы вы дали мне несколько ссылок на такую ​​реализацию.   -  person snak    schedule 01.10.2020

Ответы (2)


arrow_upward
3
arrow_downward

Этот вопрос выглядит слишком упрощенным и надуманным; было бы неплохо иметь более конкретную мотивацию. Но вот выстрел в темноте.

Мы можем определить вариант 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
person Li-yao Xia    schedule 01.10.2020
comment
Спасибо. Это то, что я имел в виду, но я не знал, как это написать. Несмотря на то, что мне по-прежнему нужно писать Y23 и Y23_ для каждой комбинации, я предпочитаю это моему g3. - person snak; 01.10.2020

arrow_upward
1
arrow_downward

Еще один подход, вдохновленный комментарием @luqui. Он похож на @li-yao-xia 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
person snak    schedule 05.10.2020