Функция GADT полиморфного типа результата

В следующем коде, что я могу заменить x = .... Обратите внимание, что я не хочу накладывать ограничение класса на a (конечно, a уже относится к типу Bool, поэтому может принимать только один из двух типов).

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

data D (a :: Bool) where
  D1 :: D True
  D2 :: D False

x :: D a
x = ...

По сути, с такими GADT легко реализовать полиморфизм на входе (просто сопоставить соответствующие конструкторы), но я хочу использовать полиморфизм на выходе.


types haskell gadt
person Clinton    schedule 22.01.2017    source источник
comment
Это невозможно, нет возможности вернуть полиморфное значение в D a, если только оно не нижнее. Если/когда мы получим pi типов (нестертые типы), то можно будет писать x :: pi a. D a   -  person chi    schedule 22.01.2017
comment
Кроме того, как это ни неприятно, D Any является допустимым типом. DataKinds по-прежнему допускает неопределенность уровня типа...   -  person Alec    schedule 22.01.2017
comment
Я не возражаю против того, чтобы быть неопределенным, пока определены x :: D True и x :: D False.   -  person Clinton    schedule 22.01.2017
comment
GHC не знает, что a :: Bool может быть только True или False. Диспетчеризация на a :: Bool невозможна никак, так как стирается во время выполнения. Вам нужно как минимум x :: SingI a => D a или x :: Sing a -> D a, если вы хотите отправить.   -  person András Kovács    schedule 22.01.2017
comment
Если a стирается во время выполнения, как работает диспетчеризация для методов класса? Или тип сохраняется для типов с ограничениями класса?   -  person Clinton    schedule 22.01.2017
comment
@Clinton Явные словари передаются, а типы стираются. Например, для чего-то вроде Show a => a -> IO () это более или менее реализовано как (a -> String) -> a -> IO (). Фактические реализации методов класса передаются в качестве аргументов, поэтому типы не должны этого делать.   -  person Justin L.    schedule 22.01.2017

Ответы (1)


arrow_upward
8
arrow_downward

Для этого требуются зависимые типы - без этого не обойтись. В Idris, языке с зависимой типизацией, похожем на Haskell, вы можете написать это просто отлично:

data D : Bool -> Type where
  D1 : D True
  D2 : D False

-- The `{ .. }` mean the argument is inferred.
x : {a : Bool} -> D a
x {a = True} = D1
x {a = False} = D2

В Haskell единственный способ диспетчеризации на основе типа во время выполнения — через классы типов, поэтому вам необходимо ограничение. На самом деле, как указывает @András, существует SingI, который создан для этого (он взят из пакета singletons, который работает именно с такой проблемой).

В вашем случае это будет:

{-# LANGUAGE GADTs, TypeInType, ScopedTypeVariables #-}

import Data.Singletons.Prelude   

data D (a :: Bool) where
  D1 :: D True
  D2 :: D False

x :: forall a. SingI a => D a
x = case sing :: Sing a of
      STrue -> D1
      SFalse -> D2

Возможно, стоит упомянуть, что, несмотря на наличие ограничения SingI, для него уже определены все соответствующие экземпляры. Все остальное, что является допустимым типом D, но не с аргументом Bool (например, D Any), терпит неудачу во время компиляции (экземпляр SingI просто не найден).

ghci> let _ = x :: D True
ghci> let _ = x :: D False
ghci> let _ = x :: D Any
<interactive> error:
  • No instance for (SingI Any) arising from a use of ‘x’
  • In the expression: x :: D Any
    In a pattern binding: _ = x :: D Any
person Alec    schedule 22.01.2017
comment
Этот ответ будет улучшен с демонстрацией техники класса типов. - person Benjamin Hodgson♦; 22.01.2017
comment
@BenjaminHodgson Обновлено соответственно. - person Alec; 22.01.2017