Могу ли я иметь аргумент полиморфной функции, который может не понадобиться для некоторых типов?

У меня есть тип данных F со специальным случаем для Int:

{-# LANGUAGE GADTs, RankNTypes #-}
data F a where
   FGen :: a -> F a
   FInt :: F Int

Без раскрытия деталей этого типа данных вызывающим абонентам - реальный тип данных более сложный, содержащий внутренние детали реализации - я хочу предоставить API для его использования:

transform :: (a -> b) -> b -> F a -> b
transform f i (FGen v) = f v
transform f i FInt = i

Если я назову transform на a F Int, очевидно, что оба первых двух аргумента важны:

transformInt :: F Int -> Int
transformInt = transform (+1) 5

Но если я назову его на F Char, второй аргумент не нужен, поскольку значение не может быть FInt:

transformChar :: F Char -> Char
transformChar = transform id (error "unreachable code")

Есть ли способ выразить это в типе transform?

Я пробовал

transform :: (a -> b) -> (a ~ Int => b) -> F a -> b
transform f i (FGen v) = f v
transform f i FInt = i

но затем transformChar не компилируется с

    Couldn't match type ‘Char’ with ‘Int’
    Inaccessible code in
      a type expected by the context: (Char ~ Int) => Char
    In the second argument of ‘transform’, namely
      ‘(error "unreachable code")’
    In the expression: transform id (error "unreachable code")
    In an equation for ‘transformChar’:
        transformChar = transform id (error "unreachable code")

и в любом случае мне бы хотелось, чтобы значение absurd могло использоваться вместо ошибки, чтобы правильно выразить, что компилятор должен иметь возможность доказать, что код никогда не будет использоваться.

Ответы

Ответ 1

Мы можем использовать пропозициональный тип равенства в Data.Type.Equality, и мы также можем выразить недоступность кода из GHC 7.8, используя пустые выражения case:

{-# LANGUAGE GADTs, RankNTypes, EmptyCase, TypeOperators #-}

import Data.Type.Equality   

data F a where
   FGen :: a -> F a
   FInt :: F Int

transform :: (a -> b) -> ((a :~: Int) -> b) -> F a -> b
transform f i (FGen v) = f v
transform f i FInt = i Refl

transformChar :: F Char -> Char
transformChar = transform id (\p -> case p of {})
-- or (\case {}) with LambdaCase

transformInt :: F Int -> Int
transformInt = transform (+1) (const 5)

Ответ 2

Мне больше нравится ответ с GADT для доказательства равенства типов. В этом ответе объясняется, как сделать то же самое с TypeFamilies. С замкнутыми типами мы можем писать функции от типов до единицы () и нулевой Void системы типов, чтобы представлять предпозиционную истину и ложь.

{-# LANGUAGE TypeFamilies #-}

import Data.Void

type family IsInt a where
    IsInt Int = ()
    IsInt a   = Void

Второй аргумент transform равен () -> b, когда IsInt a и Void -> b (тип absurd), когда a не является целым числом.

transform :: (a -> b) -> (IsInt a -> b) -> F a -> b
transform f i (FGen v) = f v
transform f i FInt = i ()

transformChar можно записать в терминах absurd, а transformInt должен проходить в b как постоянную функцию.

transformChar :: F Char -> Char
transformChar = transform id absurd

transformInt :: F Int -> Int
transformInt = transform (+1) (const 5)

Больше повторного использования

В предложении András Kovács мы можем сделать это более многоразовым с семейством типов для равенства типа (==), которое возвращает поднятый Bool s.

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}

type family (==) a b :: Bool where
    (==) a a = True
    (==) a b = False

Мы могли бы предоставить другое семейство типов для преобразования True в () и False в Void. Для этой конкретной задачи он лучше читает путь от True или False, а некоторый тип b до () -> b или Void -> b.

type family When p b where
    When True  b = ()   -> b
    When False b = Void -> b

Затем читается тип transform.

transform :: (a -> b) -> When (a == Int) b -> F a -> b