haskell - 如何解决 F# 的类型系统

Question

在 Haskell 中，您可以使用 unsafeCoerce 来覆盖类型系统。如何在 F# 中执行相同操作？

例如，实现 Y 组合器。

Answer 1

我想提供一种不同的解决方案，基于将非类型化 lambda 演算嵌入到类型化函数语言中。这个想法是创建一种数据类型，允许我们在类型 α 和 α → α 之间进行更改，从而摆脱类型系统的限制。我对 F# 不太熟悉，所以我会用 Haskell 给出答案，但我相信它可以很容易地适应(也许唯一的复杂性可能是 F# 的严格性)。

-- | Roughly represents morphism between @a@ and @a -> a@.
-- Therefore we can embed a arbitrary closed λ-term into @Any a@. Any time we
-- need to create a λ-abstraction, we just nest into one @Any@ constructor.
--
-- The type parameter allows us to embed ordinary values into the type and
-- retrieve results of computations.
data Any a = Any (Any a -> a)

请注意，类型参数对于组合术语并不重要。它只是允许我们将值嵌入到我们的表示中并稍后提取它们。特定类型Any a的所有术语都可以不受限制地自由组合。

-- | Embed a value into a λ-term. If viewed as a function, it ignores its
-- input and produces the value.
embed :: a -> Any a
embed = Any . const

-- | Extract a value from a λ-term, assuming it's a valid value (otherwise it'd
-- loop forever).
extract :: Any a -> a
extract x@(Any x') = x' x

通过这种数据类型，我们可以用它来表示任意无类型的 lambda 项。如果我们想将 Any a 的值解释为函数，我们只需解开它的构造函数即可。

首先我们定义函数应用:

-- | Applies a term to another term.
($$) :: Any a -> Any a -> Any a
(Any x) $$ y = embed $ x y

和 λ 抽象:

-- | Represents a lambda abstraction
l :: (Any a -> Any a) -> Any a
l x = Any $ extract . x

现在我们已经拥有了创建复杂 λ 项所需的一切。我们的定义模仿了经典的 λ 项语法，我们所做的就是使用 l 来构造 λ 抽象。

让我们定义 Y 组合器:

-- λf.(λx.f(xx))(λx.f(xx))
y :: Any a
y = l (\f -> let t = l (\x -> f $$ (x $$ x))
              in t $$ t)

我们可以用它来实现 Haskell 的经典 fix。首先，我们需要能够将 a -> a 函数嵌入到 Any a 中:

embed2 :: (a -> a) -> Any a
embed2 f = Any (f . extract)

现在定义起来很简单

fix :: (a -> a) -> a
fix f = extract (y $$ embed2 f)

以及随后递归定义的函数:

fact :: Int -> Int
fact = fix f
  where
    f _ 0 = 1
    f r n = n * r (n - 1)

请注意，上面的文本中没有递归函数。唯一的递归是在 Any 数据类型中，它允许我们定义 y(也是非递归定义的)。