Возврат подмножества типов в Haskell

Question

Я пытаюсь ограничить тип возвращаемого значения функции для подмножества (добрых) конструкторов. Я могу использовать классы типов для ограничения типов ввода, но когда я пытаюсь использовать ту же технику для типов возврата, как показано ниже, я получаю Couldn't match type ‘s’ with ‘'A’ ошибка.

Есть ли способ ограничить bar функция ниже, чтобы вернуть либо SomeA или же SomeB?

Кажется, что Liquid Haskell является альтернативой, но, кажется, это должно быть возможно, используя только такие вещи, как DataKinds, GADTs и / или TypeInType,

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

module Test where

data State = A | B | C

class AorB (s :: State)
instance AorB 'A
instance AorB 'B

data Some (s :: State) where
  SomeA :: Some 'A
  SomeB :: Some 'B
  SomeC :: Some 'C

-- This works
foo :: AorB s => Some s -> Bool
foo aorb = case aorb of
  SomeA -> True
  SomeB -> False

-- This fails to compile with ""Couldn't match type ‘s’ with ‘'A’""
bar :: AorB s => Some s
bar = SomeA

Answer 1

Несколько вещей здесь. Если вы компилируете с -Wall (что вы должны!) вы найдете, что ваше определение foo дает исчерпывающее предупреждение. И это должно быть, потому что, как вы определили AorB открыт". То есть кто-то в другом модуле может свободно объявить

instance AorB 'C

а потом ваше определение foo вдруг станет недействительным, так как он не может обработать SomeC дело. Чтобы получить то, что вы ищете, вы должны использовать семейство закрытого типа:

type family IsAorB s where
    IsAorB 'A = 'True
    IsAorB 'B = 'True
    IsAorB _  = 'False

Эта семья полностью определена на States. Затем мы определим ваш предыдущий AorB ограничение вот так:

type AorB s = IsAorB s ~ 'True

Однако через минуту нам нужно будет использовать AorB в карри, что недопустимо для синонимов типа. Есть идиома для объявления синонимов curriable, которая немного неуклюжа, но является лучшим, что мы имеем в данный момент:

class    (IsAorB s ~ 'True) => AorB s
instance (IsAorB s ~ 'True) => AorB s

В любом случае, с этим новым определением вы обнаружите, что неисчерпаемое предупреждение foo, Хорошо.

Теперь к вашему вопросу. Беда с вашим определением (с явным forall добавлено для наглядности)

bar :: forall s. AorB s => Some s
bar = SomeA

является то, что нам разрешено создавать bar @B, давая нам

bar @B :: AorB B => Some B
bar = SomeA

AorB B удовлетворительно, поэтому мы должны быть в состоянии получить Some B, право? Но не в соответствии с вашей реализацией. Так что здесь что-то логически не так. Вы, вероятно, хотите вернуть экзистенциально количественно sдругими словами, вы хотите bar функция, чтобы выбрать какой s это не звонящий. Неофициально

bar :: exists s. AorB s <AND> Some s

То есть, bar выбирает sи возвращает Some sвместе с некоторыми доказательствами того, что AorB s держит. Это больше не является следствием, мы бы не возлагали ответственность на вызывающего, чтобы доказать, что тип bar выбрал был либо A или же B - звонящий не знает, что было выбрано.

Haskell не поддерживает напрямую экзистенциальные типы, но мы можем моделировать их с помощью GADT (обязательно используйте PolyKinds а также ConstraintKinds)

data Ex c f where
     Ex :: c a => f a -> Ex c f

Ex c f можно прочитать как "существует a такой, что c a держит и есть значение f a". Это экзистенциально, потому что переменная a не появляется в Ex c fэто скрыто конструктором. И теперь мы можем реализовать bar

bar :: Ex AorB Some
bar = Ex SomeA

Мы можем проверить, правильно ли распространяются ограничения, передав их foo:

test :: Bool
test = case bar of Ex s -> foo s

Вот и ты.

Тем не менее, в плане дизайна я бы просто сказал

bar :: Some A

вместо. Тип подписей должен быть максимально информативным. Не скрывайте информацию, которую вы знаете - пусть абстракция скрывает. Когда вы скрываете информацию о своих предположениях / аргументах, вы укрепляете свою подпись; когда вы скрываете свои результаты, вы делаете их слабее. Сделай это сильным.

Answer 2

Вот полный рабочий код, основанный на ответе @luqui, для справки:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}

module Test2 where

data State = A | B | C

type family IsAorB (s :: State) where
  IsAorB 'A = 'True
  IsAorB 'B = 'True
  IsAorB _  = 'False

-- type AorB s = IsAorB s ~ 'True

class (IsAorB s ~ 'True) => AorB s
instance (IsAorB s ~ 'True) => AorB s

data Some (s :: State) where
  SomeA :: Some 'A
  SomeB :: Some 'B
  SomeC :: Some 'C

data Ex c f where
  Ex :: c a => f a -> Ex c f

bar :: Ex AorB Some
bar = Ex SomeA