标签: system-f

我一直在阅读各种类型的系统和lambda calculi,我发现lambda立方体中的所有类型的lambda结石都是强烈正常化而不是图灵等效.这包括系统F,简单类型的lambda演算加多态.

这引出了以下问题,我一直无法找到任何可理解的答案:

• (例如)Haskell的形式主义与表面上基于的微积分有何不同？
• Haskell中的哪些语言功能不属于System F形式主义？
• 允许图灵完整计算所需的最小变化是什么？

非常感谢你帮助我理解这一点.

如何系统地计算系统F中给定类型的居民数量？

假设有以下限制:

• 所有居民终止,即没有底部.
• 所有居民都缺乏副作用.

例如(使用Haskell语法):

• Bool 有两个居民.
• (Bool, Bool) 有四个居民.
• Bool -> (Bool, Bool) 有十六个居民.
• forall a. a -> a 有一个居民.
• forall a. (a, a) -> (a, a) 有四个居民.
• forall a b. a -> b -> a 有一个居民.
• forall a. a 没有居民.

实现前三个算法是微不足道的,但我无法弄清楚如何为其他算法做到这一点.

在系统F中,类型exists a. P可以被编码为forall b. (forall a. P -> b) -> b使用存在性的任何系统F术语可以根据关于打字和缩减规则的该编码来表达.

在"类型和编程语言"中,将显示以下练习:

我们可以根据存在类型编码通用类型吗？

我的直觉说这是不可能的,因为在某种程度上,"存在包装"机制并不像"类型抽象"机制那样强大.我如何正式展示这个？

我甚至不确定我需要证明什么才能正式显示这个结果.

下面是几个简单的函数：

f1 :: () -> ()
f1 () = ()

f2 :: a -> a
f2 a = a

f3 :: a -> (a, a)
f3 a = (a, a)

f4 :: (a, b) -> a
f4 (a, b) = a

所有的f1，f2以及f3能够接受()为输入。另一方面，当然f4不能接受()；f4 ()是类型错误。

是否有可能TYPE-理论上刻画了什么f1，f2以及f3有什么共同点？具体而言，是有可能定义一个acceptsUnit函数，以使得acceptsUnit f1，acceptsUnit f2和acceptsUnit f3是公类型的，但acceptsUnit f4是一种类型的错误-和不具有其他的效果？

下面完成了部分工作，但将其输入单态化（在 Haskell …

根据'什么是Hindley Milner',它说:

Hindley-Milner是System F的限制,它允许更多类型但需要程序员注释.

我的问题是,什么是系统F中可用的类型的例子,在Hindley Milner(类型推断)中不可用？

(假设系统F类型的推断已被证明是不可判定的)

我想得到以下示例进行类型检查:

{-# LANGUAGE AllowAmbiguousTypes    #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeFamilies           #-}

module Foo where

f :: Int -> (forall f. Functor f => Secret f) -> Int
f x _ = x

g :: (forall f. Functor f => Secret f) -> Int
g = f 4

type family Secret (f :: * -> *) :: * where
  Secret f = Int

我得知它可能无法推断和检查gs类型(即使在这种特定情况下它很明显,因为它只是一个部分应用程序):Secret不是单射的,并且没有办法告诉编译器Functor它应该期望哪个实例.因此,它失败并显示以下错误消息:

    • Could not deduce (Functor …

我不明白为什么这个程序不可打字:

type Test a = forall z. (a -> z) -> z

cons :: a -> Test a
cons = \a -> \p -> p a

type Identity = forall x. x -> x

t :: Identity
t = \x -> x

c :: Test Identity
c = cons (t :: Identity)

main :: IO ()
main = do{
  print "test"
}

我使用-XRankNTypesGHC 选项.

我有以下错误:

Couldn't match type `x0 -> x0' with `forall x. x -> x'
Expected …