我最近完成了一门大学课程,课程特色是 Haskell 和 Agda (一种依赖类型的函数式编程语言) ,我想知道是否有可能用组合子逻辑代替 lambda 微积分。使用 Haskell,这似乎可以使用 S 和 K 组合子,从而使其无点。我想知道对于阿格达来说等价物是什么。也就是说,是否可以在不使用任何变量的情况下使依赖类型的函数式编程语言等同于 Agda?
另外,有没有可能以某种方式用组合子代替量化?我不知道这是否是一个巧合,但是举个例子,全称量化使类型签名看起来像一个 lambda 表达式。有没有办法在不改变类型签名含义的情况下删除类型签名中的全称量化?例如:
forall a : Int -> a < 0 -> a + a < a
同样的事情可以在不使用 forall 的情况下表达吗?