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

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

如果我要打电话transform给a F Int,显然前两个论点都很重要:

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

但是如果我打算在a上调用它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,我们也可以使用空案例表达式来表达来自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)