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

Question

В следующем коде, что я могу заменить 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 = ... 

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

Answer 1

Для этого требуются зависимые типы - нет никакого способа обойти его. В Идрис 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