存在普遍量化的类型变量,并且存在存在量化的数据类型.然而,尽管人们exists a. Int -> a有时会给出形式的伪代码以帮助解释概念,但它似乎并不像编译器扩展那样真正引起人们的兴趣.这只是"添加这种东西没什么价值"的东西(因为它对我来说确实很有价值),或者是否存在像不确定性这样的问题,这使得它真的变得不可能.
编辑:我已经将viorior的答案标记为正确,因为它似乎可能是为什么不包含这个问题的实际原因.我想补充一些额外的评论,以防万一有人想帮助澄清这一点.
根据评论中的要求,我将举例说明为什么我认为这有用.假设我们有一个数据类型如下:
data Person a = Person
{ age: Int
, height: Double
, weight: Int
, name: a
}
所以我们选择参数化a,这是一个命名约定(我知道在这个例子中,NamingConvention使用适当的数据构造函数为美国"第一,中间,最后",西班牙语"名称,父亲姓名,母亲的名字",等等.但是现在,就这样吧."
因此,我们看到有几个函数基本上忽略了Person参数化的类型.例子就是
age :: Person a -> Int
height :: Person a -> Double
weight :: Person a -> Int
在这些基础之上构建的任何函数都可以类似地忽略该a类型.例如:
atRiskForDiabetes :: Person a -> Bool
atRiskForDiabetes p = age p + weight p > 200
--Clearly, I am not actually a doctor
现在,如果我们有一个异类的人员列表(类型[exists a. …
写在Haskell中,这里的数据类型证明一个列表是另一个列表的排列:
data Belongs (x :: k) (ys :: [k]) (zs :: [k]) where
BelongsHere :: Belongs x xs (x ': xs)
BelongsThere :: Belongs x xs xys -> Belongs x (y ': xs) (y ': xys)
data Permutation (xs :: [k]) (ys :: [k]) where
PermutationEmpty :: Permutation '[] '[]
PermutationCons :: Belongs x ys xys -> Permutation xs ys -> Permutation (x ': xs) xys
有了a Permutation,我们现在可以置换记录:
data Rec :: (u -> *) -> [u] -> * where …我想弄清楚是否有可能MutableArray#在一个紧凑的区域.ghc开发人员
和文档明确表示不这样做,
因为它允许用户指向外部的东西Compact.除此之外,我仍然有兴趣尝试这样做,理解我将负责确保数组仅指向相同的内容Compact.
我的想法是添加Array#一个紧凑区域,然后尝试使用unsafeThawArray#以下方法解冻它:
unsafeThawArray# :: Array# a -> State# s -> (#State# s, MutableArray# s a#)
我应该能够使用writeArray#,前提是(a)我写入的所有内容都MutableArray#在同一个紧凑区域中,(b)seq在将其写入数组之前,我将所有内容评估为WHNF .我认为这是安全的.我确实有一个基于
stg_unsafeThawArrayzh评论的问题:
MUT_ARR_PTRS存在于可变列表中,但是MUT_ARR_PTRS_FROZEN通常不会...
我不太了解GHC的内部结构,但这里是我对评论的理解:有一种叫做可变列表的东西,它有一堆可变数组,偶尔由GC扫描.就我的目的而言,这是有问题的,因为这意味着unsafeThawArray#将导致GC开始在紧凑区域中扫描事物.这不好.但是,也许我的理解是错误的,这将是伟大的.
如果unsafeThawArray#不能做我需要的事情,那我就是想这样unsafeCoerce#做,但我想再次听取有关这个主题的知识渊博的人的意见.谢谢,让我知道我是否可以澄清任何事情.
编辑:只是对未来读者的评论.在考虑了这个之后,我意识到使用SmallArray#而不是Array#更好.它应该使写入更快.将写入MutableArray#的代码与写入SmallMutableArray#的代码进行比较.MutableArray#当一切都在紧凑的堆上时,保持更新的卡表是毫无价值的,因为它永远不会被扫描.
我在玩耍 constraints包(对于GHC Haskell).我有一个类型系列来确定类型级列表是否包含一个元素:
type family HasElem (x :: k) (xs :: [k]) where
HasElem x '[] = False
HasElem x (x ': xs) = True
HasElem x (y ': xs) = HasElem x xs
这是有效的,但它没有给我的一点是知识
HasElem x xs entails HasElem x (y ': xs)
因为类型族不是"is element of"语句的归纳定义(就像你在agda中所拥有的那样).我很确定,在GADT可以升级到类型级别之前,没有办法用数据类型表达列表成员资格.
所以,我用这个constraints包来写这个:
containerEntailsLarger :: Proxy x -> Proxy xs -> Proxy b -> (HasElem x xs ~ True) :- (HasElem x (b ': xs) ~ True)
containerEntailsLarger _ _ _ = …在GHC.Prim,我们找到一个名为dataToTag#的神奇函数:
dataToTag# :: a -> Int#
它根据它使用的数据构造函数将任何类型的值转换为整数.这是用来加速的衍生实现Eq,Ord和Enum.在GHC源代码中,用于dataToTag#解释参数应该已经通过评估的文档:
dataToTag#primop应始终应用于已计算的参数.确保这一点的方法是通过GHC.Base中的'getTag'包装器调用它:
Run Code Online (Sandbox Code Playgroud)getTag :: a -> Int# getTag !x = dataToTag# x
对我来说,x在dataToTag#调用之前我们需要强制进行评估是完全合理的.我没有得到的是为什么爆炸模式就足够了.定义getTag只是语法糖:
getTag :: a -> Int#
getTag x = x `seq` dataToTag# x
关于评估顺序的注释:表达式
seq a b不保证将在b之前评估a.seq给出的唯一保证是在seq返回值之前将评估a和b两者.特别是,这意味着可以在a之前评估b.如果需要保证特定的评估顺序,则必须使用"并行"软件包中的函数pseq.
在软件包的Control.Parallel模块中parallel,文档进一步阐述:
...序列是它的两个参数严格,所以编译器可以,例如,重新
a `seq` b进入b `seq` a `seq` b...... …
haskell的stm库中有一个带有以下类型签名的函数:
alwaysSucceeds :: STM a -> STM ()
根据我对haskell中STM的理解,有三种方法可以在执行STM计算时"出错"(使用该术语):
retry重启来触发的.这有效地使线程阻塞,然后一旦读取集中的TVar改变就重试.throwSTM会导致这种情况.这个与前两个不同,因为事务没有重新启动.相反,错误会传播并导致程序崩溃或被IO monad捕获.如果这些是准确的(如果不是,请告诉我),我无法理解alwaysSucceeds可能做什么.该always函数似乎构建在它之上,看起来它可以写成没有alwaysSucceeds:
--This is probably wrong
always :: STM Bool -> STM ()
always stmBool = stmBool >>= check
文档alwaysSucceeds说:
alwaysSucceeds添加了一个新的不变量,当传递给alwaysSucceeds时,在当前事务结束时以及每个后续事务结束时都必须为true.如果它在任何这些点失败,那么违反它的事务将被中止,并且传播由不变量引发的异常.
但由于参数是类型STM a(多态a),因此它不能使用事务为决策制定的任何部分返回的值.所以,似乎它会寻找我之前列出的不同类型的故障.但那有什么意义呢？STM monad已经处理了故障.如何将它包装在此函数中会影响它？为什么类型的变量会a被丢弃,导致STM ()？
我试图弄清楚我有一个小ruby脚本的等效shell脚本.这是ruby脚本:
require 'openssl'
require 'base64'
k = OpenSSL::PKey::RSA.new(File.read("key.pem"))
res = File.read("res.tmp")
digest = OpenSSL::Digest::SHA256.new
signature = k.sign(digest,res)
File.write("foo1.txt",Base64.strict_encode64(signature))
而已.它需要一些数据,获取它的SHA256哈希,然后用我拥有的私钥签名.我认为终端上的等效命令应该是:
openssl sha -sha256 -sign key.pem < res.tmp | base64 -w 0 > foo2.txt
但这些不会产生相同的输出.任何人都可以告诉我为什么？
- 编辑 -
我正在添加更多信息,以便人们可以尝试在他们的计算机上重现这一点,如果需要的话.内容res.tmp是:
This is some sample text.
This is some sample text.
This is some sample text.
This is some more sample text.
This is some more sample text.
This is some more sample text.
私钥(不是实际用于任何生产系统的私钥,只是澄清它)是:
-----BEGIN PRIVATE KEY-----
MIICdgIBADANBgkqhkiG9w0BAQEFAASCAmAwggJcAgEAAoGBALNY2EtJTj78tvnL
G1v+5HFqn8mZ85AToUqj/n86/eymcMqEjskHAoVmU9FOr+ZsnSxopNvUVLCzDkv6 …我是伊德里斯的新手.我之前使用过一点agda,我在GHC Haskell中有很重的背景.我试图理解为什么在GHC Haskell中有效的东西在Idris中不起作用.以下代码无法编译(idris版本0.12.3,nobuiltins,noprelude):
data Nat = S Nat | Z
plus : Nat -> Nat -> Nat
plus Z right = right
plus (S left) right = S (plus left right)
rightIdentityAlt : (n : Nat) -> n = (plus n Z)
rightIdentityAlt Z = Refl
rightIdentityAlt (S y) = case rightIdentityAlt y of
Refl => Refl
此操作失败,并显示以下错误:
idris_binary.idr:21:3-7:当在rightIdentityAlt中检查IdrisBinary.case块的左侧时,在idris_binary.idr:20:31:统一y并加上y Z将导致无限值
大致相当的GHC haskell代码做了类型检查.如果我改为使用以下内容,我可以将Idris版本改为typecheck:
cong : (x : Nat) -> (y : Nat) -> (f : Nat -> Nat) -> x = …不使用 Continuations 进行编译描述了一种使用连接点扩展 ANF System F 的方法。GHC 本身在 Core（一种中间表示）中有连接点，而不是直接在表面语言（Haskell）中暴露连接点。出于好奇，我开始尝试编写一种语言，通过连接点简单地扩展 System F。也就是说，连接点是面向用户的。但是，我不明白论文中的打字规则。以下是我理解的部分：
?是?在几个规则。在表达式中let x:? = u in ...，u不能引用任何连接点（VBIND），因为它连接点不能返回到任意位置。JBIND。这篇论文很好地解释了这一点。这是我没有得到的。论文引入了一个符号，我将其称为“高架箭头”，但论文本身并没有明确给出名称或提及它。从视觉上看，它看起来像一个指向右侧的箭头，它位于表达式之上。粗略地说，这似乎表示“尾部上下文”（论文确实使用了这个术语）。在论文中，这些开销箭头可以应用于术语、类型、数据构造函数，甚至环境。它们也可以嵌套。这是我遇到的主要困难。有几条规则包含在头顶箭头下的类型环境。JUMP, CASE, RVBIND, 和RJBIND都包括具有这种类型环境的场所（论文中的图 2）。然而，没有一个类型规则有一个结论，其中类型环境在一个开销箭头下。所以，我看不出如何使用JUMP,CASE等，因为前提不能由任何其他规则导出。
这是问题，但如果有人有任何补充材料提供更多上下文是开销箭头约定，或者如果有人知道 System-F-with-join-points 类型系统的实现（GHC 的 IR 除外），那将也很有帮助。
我正在处理一个项目,我正在处理Prim类型类,我需要确保我编写的特定函数是专门的.也就是说,我需要确保当我调用它时,我得到一个函数的专用版本,其中
Prim字典被内联到专用定义中而不是在运行时传递.
幸运的是,这是GHC中非常了解的事情.你可以写:
{-# SPECIALIZE foo :: ByteArray Int -> Int #-}
foo :: Prim a => ByteArray a -> Int
foo = ...
在我的代码中,这种方法运行良好.但是,由于类型类是开放的,因此可能存在Prim我在编写库时尚不知道的情况.这让我想到了手头的问题.GHC用户指南的文档SPECIALIZE
提供了两种使用方法.第一个是放在SPECIALIZE定义的网站上,就像我在上面的例子中所做的那样.第二个是将SPECIALIZEpragma放在导入函数的另一个模块中.作为参考,用户手册提供的示例是:
module Map( lookup, blah blah ) where
lookup :: Ord key => [(key,a)] -> key -> Maybe a
lookup = ...
{-# INLINABLE lookup #-}
module Client where
import Map( lookup )
data T = T1 | T2 deriving( Eq, Ord …