haskell - 我可以有一个可能不需要为某些类型提供的多态函数参数吗？

Question

我有一个数据类型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

如果我要在 F Int 上调用 transform，显然前两个参数都很重要:

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 值而不是错误来正确表达编译器应该能够证明代码永远不会被使用。

Answer 1

我们可以在 Data.Type.Equality 中使用命题等式类型我们还可以使用空 case 表达式来表达 GHC 7.8 中代码的不可访问性:

{-# 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)