事实证明,虽然存在/秩为n的类型背后的思想非常简单,但正确使用它们却令人惊讶地困难。
为什么将存在类型包装成data
类型是必要的?
我有以下简单示例:
{-# LANGUAGE RankNTypes, ImpredicativeTypes, ExistentialQuantification #-}
module Main where
c :: Double
c = 3
-- Moving `forall` clause from here to the front of the type tuple does not help,
-- error is the same
lists :: [(Int, forall a. Show a => Int -> a)]
lists = [ (1, \x -> x)
, (2, \x -> show x)
, (3, \x -> c^x)
]
data HRF = forall a. Show a => HRF (Int -> a)
lists' :: [(Int, HRF)]
lists' = [ (1, HRF $ \x -> x)
, (2, HRF $ \x -> show x)
, (3, HRF $ \x -> c^x)
]
如果我注释掉
lists
的定义,代码将成功编译。如果我不注释它,我会得到以下错误:test.hs:8:21:
Could not deduce (a ~ Int)
from the context (Show a)
bound by a type expected by the context: Show a => Int -> a
at test.hs:8:11-22
`a' is a rigid type variable bound by
a type expected by the context: Show a => Int -> a at test.hs:8:11
In the expression: x
In the expression: \ x -> x
In the expression: (1, \ x -> x)
test.hs:9:21:
Could not deduce (a ~ [Char])
from the context (Show a)
bound by a type expected by the context: Show a => Int -> a
at test.hs:9:11-27
`a' is a rigid type variable bound by
a type expected by the context: Show a => Int -> a at test.hs:9:11
In the return type of a call of `show'
In the expression: show x
In the expression: \ x -> show x
test.hs:10:21:
Could not deduce (a ~ Double)
from the context (Show a)
bound by a type expected by the context: Show a => Int -> a
at test.hs:10:11-24
`a' is a rigid type variable bound by
a type expected by the context: Show a => Int -> a at test.hs:10:11
In the first argument of `(^)', namely `c'
In the expression: c ^ x
In the expression: \ x -> c ^ x
Failed, modules loaded: none.
为什么会发生这种情况?第二个例子不应该与第一个等效吗?n级别类型的这些用法有什么区别?在我需要这种多态性时,是否可能省略额外的ADT定义并仅使用简单类型?