如何解决F#的类型系统

Question

在Haskell中,您可以使用unsafeCoerce覆盖类型系统.如何在F#中做同样的事情？

例如,实现Y-combinator.

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(也是非递归定义的).