4

我正在努力解决问题，但你能在代码战上滑雪吗？它即将在 SKI 组合器中表达 lambda。来源在https://repl.it/@delta4d/SKI。

经过一些研究，尤其是组合逻辑，我能够解决除xor.

我首先将 xor 翻译成

xor x y = if y 
          then if x
               then false
               else true
          else x

这是

xor = \x y -> y (x false true) x
-- false = K I
-- true = K

将 lambda 应用于 SKI 规则，我得到了

\x.\y.y (x false true) x
\x.S (\y.y (x false true)) (K x)
\x.S (S I (K (x false true))) (K x)
S (\x.S (S I (K (x false true)))) K
S (S (K S) (\x.S I (K (x false true)))) K
S (S (K S) (S (K (S I)) (\x.K (x false true)))) K
S (S (K S) (S (K (S I)) (S (K K) (\x.x false true)))) K
S (S (K S) (S (K (S I)) (S (K K) (S (\x.x false) (K true))))) K
S (S (K S) (S (K (S I)) (S (K K) (S (S I (K false)) (K true))))) K

我检查了http://ski.aditsu.net上的 SKI 演示文稿，效果很好。

Haskell 源代码编译，但出现运行时错误。

代码战报告：

Couldn't match type `a' with `Bool' a'
  `a' is a rigid type variable bound by
      a type expected by the context: a -> a -> a at Kata.hs:66:9
Expected type: SKI
                 (Bool' a -> (Bool' a -> Bool' a -> Bool' a) -> a -> a -> a)
  Actual type: SKI (Bool' (Bool' a))
In the second argument of `xorF', namely `true'
In the second argument of `($)', namely `xorF true true'

我在本地进行了测试prettyPrintSKI $ Ap (Ap xor' false) true，它报告：

• Occurs check: cannot construct the infinite type: a20 ~ Bool' a20
  Expected type: SKI
                   (Bool' a20 -> (Bool' a20 -> Bool' a20 -> Bool' a20) -> Bool' a20)
    Actual type: SKI (Bool' (Bool' a20))
• In the second argument of ‘Ap’, namely ‘true’
  In the second argument of ‘($)’, namely ‘Ap (Ap xor' false) true’
  In the expression: prettyPrintSKI $ Ap (Ap xor' false) true

无限类型是什么？什么是刚性类型？

我在oras上做同样的事情or = \x y -> x true y，它工作得很好。

  1. https://www.codewars.com/kata/sure-but-can-you-ski-i
  2. https://en.wikipedia.org/wiki/Combinatory_logic
  3. http://ski.aditsu.net
4

1 回答 1

2

问题来自xin的双重使用λxy.y (x false true) x。它被迫同时具有两种类型。既然y使用了x，y就必须返回某种类型的东西a。现在这意味着那x false true也是 type a。所以某些类型a必须是(b -> b -> a)（对于某些b）。但这是不可能的，因为这意味着a必须包含它自己。

值得注意的是，您的解决方案是正确的。SK，只是不是 Haskell 的类型系统。所以要修复我们不需要使用x不同类型的两次。那么为什么不让它们与 相同类型λxy.y(x false true)(x true false)呢？

于 2018-04-30T12:39:42.917 回答