为了测量那些Refs的性能,我将GHC生成的组件转储到以下代码中:
import Data.IORef
main = do
r <- newIORef 18
v <- readIORef r
print v
我期望IORef完全被优化掉,只留下一个系统调用来写字符串"18"的stdout.相反,我得到250行组装.你知道有多少人会被执行吗？以下是我认为该计划的核心内容:
.globl Main.main1_info
Main.main1_info:
_c1Zi:
leaq -8(%rbp),%rax
cmpq %r15,%rax
jb _c1Zj
_c1Zk:
movq $block_c1Z9_info,-8(%rbp)
movl $Main.main2_closure+1,%ebx
addq $-8,%rbp
jmp stg_newMutVar#
_c1Zn:
movq $24,904(%r13)
jmp stg_gc_unpt_r1
.align 8
.long S1Zo_srt-(block_c1Z9_info)+0
.long 0
.quad 0
.quad 30064771104
block_c1Z9_info:
_c1Z9:
addq $24,%r12
cmpq 856(%r13),%r12
ja _c1Zn
_c1Zm:
movq 8(%rbx),%rax
movq $sat_s1Z2_info,-16(%r12)
movq %rax,(%r12)
movl $GHC.Types.True_closure+2,%edi
leaq -16(%r12),%rsi
movl $GHC.IO.Handle.FD.stdout_closure,%r14d
addq $8,%rbp
jmp GHC.IO.Handle.Text.hPutStr2_info
_c1Zj:
movl $Main.main1_closure,%ebx
jmp …我最喜欢Haskell的一个方面是编译器如何通过函数签名中的IO monad来定位副作用.但是,通过导入2个GHC原语似乎很容易绕过这种类型的检查:
{-# LANGUAGE MagicHash #-}
import GHC.Magic(runRW#)
import GHC.Types(IO(..))
hiddenPrint :: ()
hiddenPrint = case putStrLn "Hello !" of
IO sideEffect -> case runRW# sideEffect of
_ -> ()
hiddenPrint是单位类型,但它在调用时会触发副作用(它打印Hello).有没有办法禁止那些隐藏的IO(除了信任没有人导入GHC的原语)？
如适用函数的黑客中提到的那样，它们是强大的松散单曲面函数。那么，为什么它们在Haskell中的定义却不这样显示：
class Functor f => MonoidalApplicative f where
mult :: f a -> f b -> f (a,b)
unit :: a -> f a
starAp :: f (a -> b) -> f a -> f b
starAp h x = fmap (uncurry ($)) (mult h x)
<*>（starAp）可以很容易地按照乘法来重构，这个定义对我来说更简单。例如，这是Maybe实例：
instance MonoidalApplicative Maybe where
mult (Just x) (Just y) = Just (x,y)
mult _ _ = Nothing
unit x = Just x
语义近似顺序表明,如果函数f是在其参数不是一个函数时定义的,那么f在该参数中它是常量(它不使用它).但考虑这个功能,
import Control.Exception
handleAll :: SomeException -> IO ()
handleAll e = putStrLn "caught"
f :: String -> IO ()
f x = catch (putStrLn x) handleAll
f undefinedcaught在GHCi中显示,因此它看起来很明确.但是f在它的论证中并不是恒定的,因为f "test"显示test.
某处有错误吗？
根据Coq的文档
sumbool是一种布尔类型，具有其值的合理性
我认为这已经是Coq实现的直觉（或建设性）逻辑的析取性质。
例如，要证明p \/ ~pCoq中排除的中间点，您必须进行实际工作，这不是逻辑公理。因此，的证明p \/ q必须是的证明p或的证明q。
那为什么需要sumbool p q呢？
编辑
通过用精确的证据代替策略，我得到了更具体的错误消息。这个很好：
Lemma sumbool_or : forall p q : Prop, sumbool p q -> p \/ q.
Proof.
exact (fun (p q : Prop) (H : sumbool p q) =>
match H with
| left p0 => or_introl p0
| right q0 => or_intror q0
end).
Qed.
但是这个
Lemma or_sumbool : forall p q : Prop, p \/ q …鉴于这两种类型，
Inductive unit : Set := tt.
Inductive otherUnit : Set := ttt.
Coq 能证明它们是不同的吗unit <> otherUnit？
两者在排序上都是单例类型Set，因此不容易找到Set -> Prop区分它们的类型。例如，这甚至不进行类型检查
Definition singletonTT (A : Set) : Prop := forall x : A, x = tt.
因为tt有 typeunit而不是A.
我有一个std::vector<int*> v，我想防止进一步写入它。C++ 编译器不接受这个
const std::vector<const int*>& w = v;
但它接受这一点
const std::vector<const int*>& w = reinterpret_cast<const std::vector<const int*>&>(v);
后者确实适用于 Microsoft 的编译器，这意味着int*内部v和const int*内部w在内存中具有相同的地址。
这是偶然的，作为一种未指定的行为，还是有效的 C++ ？它是否适用于向量中的所有类型，例如std::vector<std::shared_ptr<int>>？如果无效，是否有另一种方法可以执行此转换？
我知道我也可以复制向量，但我想避免这种情况，因为我的向量非常大。
有一个众所周知的编译器优化，即展开后跟折叠，这称为hylomorphism（换句话说：循环）。简而言之，不是构建结构并在之后立即销毁它，而是将折叠函数直接插入到结构的生成器上，这会导致在内存中根本不创建结构的就地循环。
例如，要对用户输入的一些数字求和，我们可以这样做
let sumInput () : int =
List.fold_left (+) 0
(List.init 1875 (fun _ -> read_int ()))
中间结构是存储输入数字的列表，由List.init. 我希望 OCaml 的本机编译器ocamlopt将其优化为尾递归循环，例如
let optimSumInput () : int =
let rec optimInput_rec count sum =
if count = 0 then sum
else optimInput_rec (count-1) (sum + read_int ()) in
optimInput_rec 1875 0
但是，ocamlopt -s生成此汇编代码，我们在其中看到camlStdlib__list__init和camlStdlib__list__fold_left：
camlTestOptim__sumInput_80:
.cfi_startproc
subq $8, %rsp
.cfi_adjust_cfa_offset 8
.L102:
movq camlTestOptim__3@GOTPCREL(%rip), %rbx
movq $3751, %rax
call …即使没有扩展ExistentialQuantification,Haskell也支持一些存在类型,通过类型同构,对于任何类型类C,
(forall a. C a => (a -> b)) ~ ((exists a. C a => a) -> b)
所以函数f :: C a => a -> b需要一个x类型的参数exists a. C a.但是Haskell不允许x对某些类型的模式匹配C(通过狂野匹配完成_,因为类型类通常是无限的).
这很奇怪,因为存在类型是广义和类型.Haskell确实支持带有data关键字的有限和类型,并允许它们的模式匹配.在C++,Java和C#等语言中,存在类型是接口,它们支持使用dynamic_cast或等关键字进行模式匹配instanceof.
Haskell没有为f上述函数实现模式匹配的原因吗？
我的确切示例是并行化这种树聚合,其中信息从叶子流向根:
aggregate :: ([a] -> a) -> Tree a -> Tree a
aggregate _ (Node x []) = Node x []
aggregate aggregator (Node _ children) =
let agChildren = map (aggregate aggregator) children in
Node (aggregator $ map (\(Node y _) -> y) agChildren) agChildren
我希望聚合器函数的每个应用程序都在不同的线程上处理.所以我想想改变上面的代码,以便它生成一个依赖任务树并将它们提供给一个线程池.
我不希望某个节点受到影响,等待子线程完成.相反,这个等待的线程应该计算树中的其他可用子节点.同时为每个节点运行一个线程也太慢了.我的树可以有数百个节点,我的机器只有8个核心:他们会花时间安排而不是计算.我需要一个只在其他任务完成时才使用任务的线程池.
如下面的ErikR所提到的,parMap似乎正是这样做的.我尝试了它并用strat 64 + RTS -N2执行它,以获得完全相同的计算时间.这是代码(只是为了测试性能而进行愚蠢的计算),你明白为什么时间不会改变吗？
slowAggregate :: [Int] -> Int
slowAggregate l = let s = sum l in
sum [a + b + c | a <- [0..s], b …假设我想定义Mod4模4的整数类型.毕竟,Int是Mod2^64.我能走的一个显而易见的方法是
data Mod4 = ZeroMod4 | OneMod4 | TwoMod4 | ThreeMod4
不过我也可以这样做
data Mod4 = Mod4 Integer
instance Eq Mod4 where
(Mod4 x) == (Mod4 y) = (x-y) `mod` 4 == 0
但是这个功能有问题:
f :: Mod4 -> Mod4
f (Mod4 x) = if x < 20 then Mod4 0 else Mod4 1
f (Mod4 16)不同于f (Mod4 20),而这两个论点是==.所以我最终得到了两种平等:在记忆中的表现(
Mod4 16不同于Mod4 20)和==.
由于所有函数都可以匹配其参数,因此它们始终可以绕过任何==运算符.为什么Haskell没有将内存中的表示作为平等的定义？这样所有类型都变得平凡.
实际上,功能的概念暗示了平等:在给定相等输入时产生相等输出的图形.因此,谈论一个不相等的类型的函数是没有意义的.