Dav*_*vid 3 haskell rank-n-types
rankN从这里使用:
{-# LANGUAGE RankNTypes #-}\nrankN :: (forall n. Num n => n -> n) -> (Int, Double)\nrankN f = (f 1, f 1.0)\nRun Code Online (Sandbox Code Playgroud)\n为什么做不到map rankN [negate]?有什么方法可以让它成为可能吗?
我想我现在(大部分)理解了 RankNTypes,并且看到我可以同时执行rankN (+1)和 rankN negate。
(当我认为没有涉及任何问题时,为什么会map rankN [negate]给出一个奇怪的错误?)Couldn\'t match type \xe2\x80\x98n\xe2\x80\x99 with \xe2\x80\x98Integer\xe2\x80\x99Integer
另外,我刚刚检查过:t map rankN。它给出了可怕的Couldn\'t match type \xe2\x80\x98a\xe2\x80\x99 with \xe2\x80\x98n -> n\xe2\x80\x99 because type variable \xe2\x80\x98n\xe2\x80\x99 would escape its scope. This (rigid, skolem) type variable is bound by...。我看到在某些情况下该错误是如何发生的,但并不真正理解为什么它会适用于此。
谢谢,如果这是重复的,很抱歉。(但我无法在所有其他 RankNTypes 问题中找到答案。)
\n默认情况下它不起作用的原因是因为映射的类型是(a -> b) -> [a] -> [b],但在本例中您无法将其实例a化为涉及 的类型。这种实例化称为谓式(impredicative),GHC 很长一段时间(可靠地)不支持它。forallforall n. Num n => n -> n
自 GHC 9.2.1 以来,有一个新的可靠的扩展实现ImpredicativeTypes,它允许您立即实例化:
GHCi, version 9.2.0.20210821: https://www.haskell.org/ghc/ :? for help
ghci> :set -XImpredicativeTypes
ghci> :t rankN
rankN :: (forall n. Num n => n -> n) -> (Int, Double)
ghci> :t map rankN
map rankN :: [forall n. Num n => n -> n] -> [(Int, Double)]
ghci> :t map rankN [negate]
map rankN [negate] :: [(Int, Double)]
ghci> map rankN [negate]
[(-1,-1.0)]
Run Code Online (Sandbox Code Playgroud)
| 归档时间: |
|
| 查看次数: |
49 次 |
| 最近记录: |