小编V. *_*ria的帖子

Haskell 接受以下类型的定义

data Lam = Func (Lam -> Lam)

它旨在表示无类型的 lambda-terms。例如，Church 的布尔值就是这种类型

trueChurch :: Lam
trueChurch = Func (\x -> Func (\y -> x))
falseChurch :: Lam
falseChurch = Func (\x -> Func (\y -> y))

构造函数Func :: (Lam -> Lam) -> Lam有这个反函数

lamUnfold :: Lam -> (Lam -> Lam)
lamUnfold (Func f) = f

这两个函数定义了Lam -> Lam和之间的类型同构Lam。当我们观察这些类型的基数（大小）时，这是令人惊讶的。由于上面的 Church 布尔值， 的基数Lam至少为 2，因此Lam -> Lam中的元素比 中的元素多Lam -> Bool …

在类别理论中,monad是两个伴随函子的组合.例如,Maybe monad是由遗忘函子组成的自由尖集函子.同样,List monad是由健忘的仿函数组成的免费monoid仿函数.

Monoid是最简单的代数结构之一,所以我想知道编程是否可以从更复杂的代数中受益.我没有在标准的Haskell包中找到自由组monad,所以我将在这里定义它

data FreeGroup a = Nil | PosCons a (FreeGroup a) | NegCons a (FreeGroup a)

的==操作者被定义为使得NegCons x (PosCons x y) == y.因此,在length :: FreeGroup a -> Int每个中,每个PosCons被计数+1并且每个NegCons-1(它是Int的唯一组态射,其在每个PosCons上的值+1).

在列表(自由幺半群)中,concat只是乘法,map是函数的函数提升.因此monad实例与of的实例FreeGroup完全相同List.

自由组monad是否有任何编程用途？此外,通常会将monad解释为上下文中的值:因为List上下文将是选择或不确定性.对于自由组monad有这样的解释吗？

免费铃声和向量空间(总是免费的)怎么样？

对于任何代数结构S,分类自由函子 FS :: Set -> S的存在意味着Haskell调用fold函数的存在:

foldS :: S s => (a -> s) -> FS a -> s

它基于自由对象 …

I was wondering whether Coq defined the real numbers as Cauchy sequences or Dedekind cuts, so I checked Coq.Reals.Raxioms and... none of these two. The real numbers are axiomatized, along with their operations (as Parameters and Axioms). Why is it so?

Also, the real numbers tightly rely on the notion of subset, since one of their defining properties is that is every upper bounded subset has a least upper bound. The Axiom completeness encodes those subsets as Prop …

假设我有两个以下类型的Haskell函数,并激活了ExplicitForAll,

f :: forall a. (a -> Int)
g :: forall a. (Int -> a)

在我看来,该类型g是同构Int -> (forall a. a)的,因为例如类型g(2)为forall a. a.

但是,类型f看起来并不是同构的(forall a. a) -> Int.f是一个多态函数,它知道在每个输入类型上计算什么a,在数学中我想它宁可是一系列函数; 但我认为它不能处理具有所有类型的单个参数.

是类型lambda演算的规则,类型量词分布在函数目标类型上,而不是函数源类型上吗？

该类型是否(forall a. a) -> Int存在于Haskell中,可能限制为类型类(forall a. SomeClass a => a) -> Int？它有用吗？

在维基百科中,底部类型简单地定义为"没有值的类型".但是,如果b这是空类型,那么产品类型(b,b)也没有值,但似乎不同b.我同意bottom无人居住,但我不认为这个属性足以定义它.

通过库里 - 霍华德的对应,底部与数学虚假相关联.现在有一个逻辑原则说明从False跟随任何命题.通过库里 - 霍华德,这意味着这种类型forall a. bottom -> a是有人居住的,即存在一系列功能f :: forall a. bottom -> a.

那些功能是f什么？它们是否有助于定义底部,可能是所有类型的无限产品forall a. a？

根据Haskell 2010语言报告,其类型检查器基于Hindley-Milner.所以考虑f这种类型的功能,

f :: forall a. [a] -> Int

例如,它可以是长度函数.根据Hindley-Milner的说法,f []键入检查Int.我们可以通过实例的类型证明这一点f来[Int] -> Int,和类型[]来[Int],然后得出结论,应用([Int] -> Int) [Int]的类型的Int.

在这个证明中,我选择实例化类型forall a. [a] -> Int并forall a. [a]替换Int为a.我可以替代Bool,证明也可以.在Hindley-Milner中,我们可以将多态类型应用于另一个,而不指定我们使用的实例,这不奇怪吗？

更具体地说,Haskell中的什么阻止我a在实现中使用类型f？我可以想象这f是一个等于18任何的函数[Bool],并且等于所有其他类型列表上的通常长度函数.在这种情况下,会f []是18或0？Haskell报告称"内核未正式指定",因此很难说.

除了Haskell之外还有其他语言,例如Coq,它们禁止使用底层undefined或者无限递归定义

bot :: forall a. a
bot = bot

没有底部的好处很简单:所有程序都终止.编译器保证没有无限循环,没有无限递归.

还有一个不那么明显的好处:语言的逻辑(由库里 - 霍华德对应给出)是一致的,它不能证明是矛盾的.因此,相同的语言可以编写程序和程序正确的证明.但这可能是偏离主题的.

对无限递归的保护也很简单:强制每个递归定义都有参数(这里bot没有),并强制递归调用减少其中一个参数.这里减少的是代数数据类型,被视为构造函数和值的有限树.Coq的编译器检查递减参数是否为ADT(data在Haskell中),并且递归调用是在参数的子case of树上完成的,通常是通过a ,而不是来自其他地方的其他树.

现在这种语言约束的成本:我们失去了图灵完整性(因为我们无法解决暂停问题).这意味着有终止函数,可以使用一般递归在Haskell中编码,这将被编译器拒绝.然而,在实践中,Coq库的大小表明很少需要那些奇特的功能.有人甚至知道其中一个吗？

有些情况下无限循环是有意义的:

• 用户通过在键盘上单击或键入来发出命令的交互式程序通常会永远运行.他们等待命令,处理它然后等待下一个命令.直到时间结束,或者更严重,直到用户发出quit命令.
• 同样,不是处理无限的用户命令流,而是处理无限的数据流.比如对数据库的连续查询.

这些案例非常具体,可能会被新的语言原语处理.Haskell介绍IO了跟踪不安全的交互.为什么不在函数签名中声明无限循环的可能性？或者将复杂程序拆分为DSMS,调用Haskell函数进行纯计算？

编辑

这是一个算法示例,如果我们切换到总编程,可能会澄清哪些更改.Euclid用于计算2个数字的GCD的算法,首先是简单的递归Haskell

euclid_gcd :: Int -> Int -> Int
euclid_gcd m n = if n <= 0 then m else euclid_gcd n (m `mod` n)

关于这个函数可以证明两件事:它终止了,它确实计算了m和n的GCD.在接受证明脚本的语言中,我们会给编译器一个证据(m mod n) < n,使得它推断递归在第二个参数上减少,因此终止.

在Haskell中,我怀疑我们能做到这一点,所以我们可以尝试以结构递归的形式重写这个算法,编译器可以很容易地检查.这意味着必须在某个参数的前任上进行递归调用.这里m mod n不会这样做,所以看起来我们被卡住了.但是与尾递归一样,我们可以添加新的参数.如果我们找到递归调用数量的界限,我们就完成了.绑定不必是精确的,它只需要高于实际的递归调用数.这种约束论证通常variant在文献中被称为,我个人称之为fuel.当耗尽燃料时,我们强制递归以错误值停止.在这里我们可以取两个数字中的任何一个的继承者: …

我必须在Haskell中对大整数矩阵的行进行排序,然后我开始使用随机数据进行基准测试.我发现Haskell比C++慢3倍.

由于随机性,我希望行比较总是在第一列终止(它应该没有重复).因此,我将矩阵缩小为实现为Vector(Unboxed.Vector Int)的单个列,并将其排序与通常的Vector Int进行比较.

Vector Int尽可能快地排序C++(好消息!),但同样,列矩阵慢了3倍.你知道为什么吗？请在下面找到代码.

import qualified Data.Vector.Unboxed as UV(Vector, fromList)
import qualified Data.Vector as V(Vector, fromList, modify)
import Criterion.Main(env, bench, nf, defaultMain)
import System.Random(randomIO)
import qualified Data.Vector.Algorithms.Intro as Alg(sort)

randomVector :: Int -> IO (V.Vector Int)
randomVector count = V.fromList <$> mapM (\_ -> randomIO) [1..count]

randomVVector :: Int -> IO (V.Vector (UV.Vector Int))
randomVVector count = V.fromList <$> mapM (\_ -> do
                                               x <- randomIO
                                               return $ UV.fromList [x]) [1..count]

benchSort :: IO ()
benchSort = do …

我有点困惑需要多少反斜杠才能|在 grep 的正则表达式中转义交替运算符。这个

echo abcdef | grep -e"def|zzz"

不输出任何内容，因为 grep 不处于扩展正则表达式模式。用一个反斜杠转义，

echo abcdef | grep -e"def\|zzz"

打印abcdef。更令人惊讶的是，用 2 个反斜杠转义也有效，

echo abcdef | grep -e"def\\|zzz"

打印abcdef。用三个反斜杠转义失败，

echo abcdef | grep -e"def\\\|zzz"

什么都不打印。

有没有人有解释，特别是对于 2-backslash case？

编辑：

使用这个简单的参数打印程序，

void main(int argc, char** argv)
{
    for (int i = 0; i < argc; i++)
        printf("Arg %d: %s\n", i, argv[i]);
}

我调查了我的 shell 用上面的命令行做了什么：

-e"def|zzz" 变成 -edef|zzz

-e"def\|zzz" 变成 -edef\|zzz

-e"def\\|zzz" 变成 -edef\\|zzz

-e"def\\\|zzz" 变成 -edef\\\|zzz

所以所有的双引号都被删除了，反斜杠和管道不会被 shell …

Coq的标准库表示此归纳类型给出Peano自然数：

  Inductive nat :=
  | O : nat
  | S : nat -> nat.

听起来不错，因为我们可以在Coq中证明Peano的所有公理nat，包括归纳原理（由Coq给出）nat_ind。

但是这个回购声称它在古德斯坦定理的 Coq中有一个证明。而且我们知道，该定理不能仅用Peano的公理来证明。因此，似乎Coq的nat强于Peano的公理，它更像是它们的模型，其中Goodstein定理是正确的。它是否正确 ？

Coq是否可以证明与natZFC集合论在标准自然数上所做的算术定理相同？如果我们在Coq中添加经典逻辑，则存在相同的问题：

Axiom excluded_middle : forall P : Prop, P \/ ~P.

背后的根本问题是Coq证明的真实性。他们给予什么保证？我是一名开发人员，所以我对程序的证明特别感兴趣，因此对算术特别感兴趣。