Когда использовать экзистенциальный тип против зависимой пары в Haskell?

illabout спросил: 28 марта 2018 в 02:11 в: haskell

Когда вы хотите использовать специализированный экзистенциальный тип против зависимой пары (также называемой зависимой суммой или сигма-типом)?

Вот пример.

Следующие представляет собой список индексированных по длине и зависимую от них функцию репликации. См. этот другой вопрос о том, как реализовать replicateVect. Ниже приведена библиотека singletons:

data Vect :: Type -> Nat -> Type where
  VNil :: Vect a 0
  VCons :: a -> Vect a n -> Vect a (n + 1)replicateVect :: forall n a. SNat n -> a -> Vect a n

Существует (по крайней мере) два возможных способа создания функции репликации, которая принимает нормальный Natural, а не singleton SNat.

Один из способов - создать специализированный экзистенциальный тип для Vect. Я называю этот SomeVect, следуя соглашениям singletons:

data SomeVect :: Type -> Type where
  SomeVect :: forall a n. Vect a n -> SomeVect areplicateExistentialVect :: forall a. Natural -> a -> SomeVect a
replicateExistentialVect nat a =
  case toSing nat of
    SomeSing sNat -> SomeVect $ replicateVect sNat a

Другой способ - использовать зависимую пару. Это использует тип Sigma из singletons:

replicateSigmaVect :: forall n a. Natural -> a -> Sigma Nat (TyCon (Vect a))
replicateSigmaVect nat a =
  case toSing nat of
    SomeSing sNat -> sNat :&: replicateVect sNat a

Эти функции выглядят очень схожими. Использование replicateExistentialVect и replicteSigmaVect также очень похоже:

testReplicateExistentialVect :: IO ()
testReplicateExistentialVect =
  case replicateExistentialVect 3 "hello" of
    SomeVect vect -> print vecttestReplicateSigmaVect :: IO ()
testReplicateSigmaVect =
  case replicateSigmaVect 3 "hello" of
    _ :&: vect -> print vect

Полный код можно найти здесь.


Это приводит меня к моим вопросам.

  1. Когда мне следует использовать специализированный экзистенциальный тип (например, SomeVect) против зависимой пары (например, Sigma)?
  2. Существуют ли какие-либо функции, которые могут только записываться с одним или другим?
  3. Есть ли какие-либо функции, которые значительно легче писать с одним или другим?

1 ответ

Есть решение
Ryan Scott ответил: 29 марта 2018 в 03:16
  1. Когда мне следует использовать специализированный экзистенциальный тип (например, SomeVect) против зависимой пары (например, Sigma)?

На этот вопрос сложно ответить, потому что:

  1. Sigma сама по себе является формой специализированного экзистенциального типа.
  2. Существует бесконечно много способов создания специализированных экзистенциальных типов - SomeVect и Sigma - только два примера этого явления.

Тем не менее, это создается впечатление, что Sigma несколько отличается от других способов кодирования экзистенциальных типов в GHC. Давайте попробуем выяснить, что именно делает его отличным.

Во-первых, давайте выпишем определение Sigma во всей его красе:

    data Sigma (s :: Type) :: (s ~> Type) -> Type where
      (:&:) :: forall s (t :: s ~> Type) (x :: s).
               Sing x -> Apply t x -> Sigma s t

И для сравнения я также определю "типичный" экзистенциальный тип:

    data Ex :: (s -> Type) -> Type where
      MkEx :: forall s (t :: s -> Type) (x :: s).
              t x -> Ex t

Давайте рассмотрим различия между ними:

  1. Sigma s t имеет два аргумента типа, тогда как Ex t имеет только один. Это не очень большая разница, и на самом деле вы могли бы написать Sigma, используя только один аргумент:

    data Sigma :: (s ~> Type) -> Type where
      (:&:) :: forall s (t :: s ~> Type) (x :: s).
               Sing x -> Apply t x -> Sigma t
    

    или Ex используя два аргумента:

    data Ex (s :: Type) :: (s -> Type) -> Type where
      MkEx :: forall s (t :: s -> Type) (x :: s).
              t x -> Ex s t
    

    Единственная причина, по которой я решил использовать два аргумента в Sigma, - это более точное соответствие представления зависимых пар в других языках, такой как в DPair Идриса. Это также, возможно, делает более ясной аналогию между Sigma s t и ∃ (x ∈ s). t(x).

  2. Гораздо важнее, вид Sigma

    Что такое символы нефункционализации и зачем они нужны? Они объяснены в разделе 4.3 статьи Продвижение функций для ввода семейств в Haskell , но я постараюсь дать сокращенную версию здесь. По сути, мы хотим иметь возможность писать семейства типов, такие как:

    type family Positive (n :: Nat) :: Type where
      Positive Z     = Void
      Positive (S _) = ()
    

    и иметь возможность использовать тип Sigma Nat Positive. Но это не сработает, поскольку вы не можете частично применить семейство типов, например, Positive. К счастью, уловка дефункционализации позволяет нам обойти эту проблему. Используя следующие определения:

    data TyFun :: Type -> Type -> Typetype a ~> b = TyFun a b -> Type
    infixr 0 ~>type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
    

    Мы можем определить символ нефункционализации для Positive, который позволит нам частично применить его:

    data PositiveSym0 :: Nat ~> Type
    type instance Apply PositiveSym0 n = Positive n
    

    Теперь в типе Sigma Nat PositiveSym0 второе поле имеет тип Apply PositiveSym0 x или просто Positive x. Таким образом, (~>) в некотором смысле более общий, чем (->), поскольку он позволяет нам использовать больше типов, чем было бы (->).

    (Если это помогает, можно думать о (~>) как о типе несопоставимых функций, как описано в разделе 4.2.4 тезиса Ричарда Эйзенберга, тогда как (->) - это тип сопоставимых функций.)

  3. Хотя конструктор MkEx имеет только одно поле, Конструктор (:&:) имеет дополнительное поле (типа Sing x). Для этого есть две причины. Во-первых, сохранение этого дополнительного поля, по определению, является частью того, что делает Sigma зависимой парой, и это позволяет нам получить его с помощью функции projSigma1. Другая причина заключается в том, что если вы вынули поле Sing x:

    data Sigma (s :: Type) :: (s ~> Type) -> Type where
      (:&:) :: forall s (t :: s ~> Type) (x :: s).
               Apply t x -> Sigma s t
    

    Тогда для этого определения потребуется AllowAmbiguousTypes в качестве x неоднозначна. Это может быть обременительным, поэтому наличие явного поля Sing x позволяет избежать этого.


Теперь, когда я закончил свое многословное объяснение, позвольте мне попытаться ответить на ваши вопросы:

  1. Когда мне следует использовать специализированный экзистенциальный тип (например, SomeVect) против зависимой пары (например, Sigma)?

Я думаю, что в конечном итоге это вопрос личного вкуса. Sigma хорош, потому что он чертовски общий, но вы можете обнаружить, что определение специализированного экзистенциального типа облегчает понимание вашего кода. (Но см. Также предостережения ниже.)

  1. Существуют ли какие-либо функции, которые могут быть написаны только одной или другой?

Я полагаю, что мой предыдущий пример Sigma Nat PositiveSym0 будет считаться чем-то, что вы не можете сделать с Ex, так как он требует использования вида (~>) , С другой стороны, вы могли бы точно так же определить:

data SomePositiveNat :: Type where
  SPN :: Sing (n :: Nat) -> Positive n -> SomePositiveNat

Так что вам технически не нужно (~>) делать это.

Кроме того, я не знаю, как написать projSigma1 эквивалент для Ex, так как он не хранит достаточно информации, чтобы написать это.

С другой стороны, Sigma s t требует наличия экземпляра Sing для вида s, поэтому если его нет , Sigma, вероятно, не будет работать.

  1. Существуют ли какие-либо функции, которые значительно проще написать с одной или другой? литий> ол>

Вам будет легче использовать Sigma, когда вам будет необходимо использовать что-то с (~>), потому что именно там оно и светит. Если ваш тип может обойтись только с видом (->), может быть удобнее использовать "типичный" экзистенциальный тип, такой как Ex, потому что в противном случае вам придется вводить шум в форму TyCon, чтобы поднять что-то вроде s -> Type в s ~> Type.

Кроме того, Sigma может оказаться проще Работайте, если важно иметь возможность удобного извлечения поля типа Sing x.

dfeuer ответил: 29 марта 2018 в 05:13
Конечно, специализированная экзистенция может также предлагать две области. data SomeVec a where SV :: SNat n -> Vec n a -> SomeVec a.