幽灵类型混乱？

Question

我对幻像类型的使用感到困惑：

type Words = String
type Numbers = Int

data NonPhantom = NP1 Words | NP2 Numbers deriving (Show)

data Phantom a = P1 Words | P2 Numbers deriving (Show) 

nonPhantomFunction :: NonPhantom -> Int
nonPhantomFunction r = 100


phantomFunction :: Phantom Numbers -> Int
phantomFunction a = 2001


main = do
   print $ nonPhantomFunction (NP1 "sdsdds") --can also pass NP2 here! 
   print $ phantomFunction (P1 "sdsdsd") --This shouldn't work!?

我希望此代码 NOT 可以编译，因为 phantomFunction 明确声明其期望数据类型 Phantom 为 Numbers。

但是这样编译好吗？我做错了什么？

Answer 1

data Phantom a = P1 Words | P2 Numbers deriving (Show)

这使得 P1 "aa" 具有任何形式的 Phantom a，对于任何 a，包括 Numbers。

Answer 2

构造函数的参数与构造函数所属类型的类型参数之间没有隐式连接。如果希望类型参数表示的类型出现在构造函数的参数中的任何位置，则需要显式声明它。

您也可以在以下表达式中看到这一点：

Nothing
[]

第一个可以为任何 a 创建一个 Maybe a，第二个可以为任何 a.

创建一个列表 [a]

同样

P1 "xyz"

根据您的示例可以为任何 a

创建一个 Phantom a

Answer 3

其他答案已经说明了你的构造函数的类型

P1 :: Words -> Phantom a

意味着它能够为任何选择a构造一个P1 a类型的值；特别是 a ~ Numbers 的选择。这就是为什么你的函数调用

phantomFunction (P1 "sdsdsd")

类型检查。

现在，你是如何解决这个问题的？我假设你想要 P1 :: Words -> Phantom Words？ GADT 允许您通过允许您编写

来约束出现在构造值类型中的类型变量

{-# LANGUAGE GADTs #-}
data Phantom a where
    P1 :: Words -> Phantom Words
    P2 :: Numbers -> Phantom Numbers

这将

确保 P1 _ 的类型为 Phantom Words，这样你就不能用它构造 Phantom Numbers
允许使用 Phantom Words 的函数通过仅匹配 P1

允许在 Phantom a 上具有多态性的函数基于模式匹配优化它们的类型（这是最重要的），因此您可以编写例如

dup :: Phantom a -> a
dup (P1 ws) = ws ++ ws -- Here, we have to return a Words, and ws is a Words, so ++ will work
dup (P2 n) = n + n -- Here, we have to return a Numbers, and x is a Numbers, so + will work

幽灵类型混乱？

Phantom type confusion?

haskell

phantom-types