小编Mai*_*tor的帖子

请注意以下计划:

data Box = Box Int
initial         = Box 1
stepper (Box x) = Box (x+1)
getter  (Box x) = x
run 0 state     = []
run n state     = getter state : run (n-1) (stepper state)
main            = print $ sum $ run 50000000 initial

在这里,run显然是线性的,因为它是一个递归0到n并且stepper是一个恒定的时间函数.您可以通过更改常量来验证 - 运行时线性比例变化.现在,请注意以下代码:

initial' box      = box 1
stepper' box box_ = box (\ x -> (box_ (x+1)))
getter' box       = box (\ x -> x) …

文章更简单,更容易!声称即使没有"Pi"存在也可以对依赖类型系统进行编码 - 也就是说,你可以重复使用"Lam"构造函数.但是,如果在某些情况下对"Pi"和"Lam"的处理方式不同,那又怎么可能呢？

此外,可以删除"明星"吗？我认为你可以用"λx.x"(id)替换它的所有出现.

每个人都知道在依赖类型的函数语言中表达自然数的优雅方式:

data Nat = Zero | Succ Nat

整数,分数,实数,复数和四元数对于实际编程应用也非常重要.可以将它们实现为:

data Integer    = Integer (sign : Bool) (modulus : Nat)
data Fraction   = Fraction (dividend : Nat) (divisor : Nat)
data Real       = Real (exponent : Integer) (fraction : Nat)
data Complex    = Complex Real Real
data Quaternion = Quaternion Real Real Real Real

但是这些都没有真正像Nats那样有意义地反映其类型的实际结构/性质.例如,整数与实际整数不同构(因为零出现两次).Reals需要超过一百万个细胞存储(3.141592),但是甚至不需要100个存储(4096),这看起来是不平衡的.复杂只是Reals的一个元组,它并不真正反映复杂的东西.我想知道在函数式编程语言中表达数字塔的自然,优雅方式是什么？

如果我正确地理解了Curry-Howard的同构,那么每个依赖类型都对应一个定理,实现它的程序就是一个证明.这意味着任何数学问题,例如a^n + b^n = c^n可以以某种方式表达为一种类型.

现在,假设我想设计一个生成随机类型(定理)的游戏,并且游戏必须尝试实现这些类型的程序(证明)(定理).是否有可能控制那些定理的难度？即,简单模式将产生平凡定理,而硬模式将产生更难的定理.

在Erastosthenes论文的真正筛选中,作者使用有限大小的轮子跳过检查筛子结构上的前N个素数的倍数.例如,为了避免检查倍数2, 3,您可以从5,然后交替添加2和4.这是wheel 2以下内容:

-- wheel 0 = ([2],[1])
-- wheel 1 = ([3,2],[2])
-- wheel 2 = ([5,3,2],[2,4]) -- "start at 5, add 2, 4, 2, 4..."
-- wheel 3 = ([7,5,3,2],[4,2,4,2,4,6,2,6])

她的车轮在筛分过程启动时完全生成.这是一个权衡,因为更大的轮子需要更多的内存.不过,我发现轮子生成背后的潜在机制本身很有趣.鉴于其明显的重复性质,我想知道是否有可能创造一个"无限轮",就像筛子一样,它呈现为一条流？我想,这个流将是列表序列的限制[1], [2], [2, 4], [4, 2, 4, 2, 4, 6, 2, 6]...- 并且可能作为primes自身的实现.

去年我问过" 依赖类型可以证明你的代码在规范上是正确的.但是你如何证明规范是正确的？ ".投票最多的答案提出以下推理:

希望你的规范很简单,小到足以通过检查来判断,而你的实现可能要大得多.

这种推理对我来说很有意义.Idris是测试这些概念最容易理解的语言; 然而,由于它几乎可以像Haskell一样使用,它常常让程序员在旧概念中游荡,而不知道在哪里应用依赖类型.一些现实世界的例子可以对此有所帮助,那么,在实践中发生的程序的具体例子是什么,很容易表达为类型,但实现起来很复杂？

有一些方法,如Q.reduce和Q.all这有助于展平诺言的异类集合的特定情况下诺言链.但请注意,通用案例:

const F = (x) => x;
const a = F(1);
const b = F(2);
const c = F(a + b);
const d = F(a + c);
const e = F(b + c);
console.log(e); 

也就是说,每个术语依赖于任意先前定义的术语的一系列赋值.假设这F是一个异步调用:

const F = (x) => Q.delay(1000).return(x);

在没有生成缩进金字塔的情况下,我无法想到表达该模式:

F(100).then(a =>
  F(200).then(b =>
    F(a+b).then(c =>
      F(a+c).then(d =>
        F(b+c).then(e =>
          F(d+e).then(f =>
            console.log(f)
          )
        )
      )
    )
  )
);

请注意,使用返回的值不起作用:

F(100).then(a => F(200))
    .then(b => F(a+b))
    .then(c => F(a+c))
    .then(d => F(b+c)) …

给定一个整数n,我如何构建包含所有长度列表的列表,n^2其中包含n每个整数的完全副本x < n？例如,因为n = 2,我们有:

[0,0,1,1], [0,1,0,1], [1,0,0,1], [0,1,1,0], [1,0,1,0], [1,1,0,0]

这可以轻松完成合并permutations和nub:

f :: Int -> [[Int]]
f n = nub . permutations $ concatMap (replicate n) [0..n-1]

但这太低效了.有没有简单的方法来编码高效/直接算法？

依赖类型Lambda编码论文的自我类型(由Peng Fu和Aaron Stump提出)提出了自我类型,据推测,它足以在构造微积分上编码归纳原理和Scott编码数据类型,而不会使系统不一致或引入悖论.

那篇论文的符号太重了,我无法完全理解如何实现它.

究竟什么是Fix和Self的主要区别？或者,换句话说:在什么点上应该限制天真实施的Fix,以便它不会在核心演算上留下任何不一致？

函数式编程语言（如 Haskell）允许用户使用等式表示法来定义函数，其中左侧有多个可以匹配的模式参数，具有任意多个嵌套。例如：

(fun (Ctr A A) (Foo (Tic X)) a b c d e) = a
(fun (Ctr A B) (Foo (Tac Y)) a b c d e) = b
(fun (Ctr B A) (Bar (Tic X)) a b c d e) = c
(fun (Ctr B B) (Bar (Tac Y)) a b c d e) = d
(fun x         y             a b c d e) = (df x y a b c d e)

不过，假设您想要将该函数编译为不允许嵌套模式匹配的语言。也就是说，您必须将这些子句扁平化为一系列函数，这些函数组合在一起，相当于fun. 例如，在上面的情况下，您可以按如下方式将其展平：

(fun …