问题标签 [type-theory]

假设我有以下（愚蠢的）课程：

我可以提供以下[]实例：

RHS 的类型[a] -> [a]应该与 统一[a] -> [b]，但 GHC 不这么认为：

我在这里想念什么？

提前致谢。

在 Racket 的主页上，他们展示了这个例子：

我知道，对于出现类型，类似这样的表达式将在真正的分支中(if (string? v) ...)标记v为具有类型。String这是因为它的类型string?有一个过滤器：

因此，为了使“高阶出现类型”与该filter函数一起使用，我希望类型filter表示谓词类型上的过滤器被传播到结果类型。但是当我检查filterREPL 中的类型时，这并没有出现：

但这不可能是真正的类型filter，因为没有限制b！我期待像

tldr：为什么filter出现的返回类型中有一个不受约束的类型变量？

编辑：我正在使用 Racket v6.0

在 System F 中，多态类型的类型是*（因为这是 System F 中唯一的类型......），例如对于以下封闭类型：

我想在 Agda 中表示 System F，因为一切都在 中*，我想我会将类型（如上）解释为 Agda Sets; 所以像

但是，Agda 没有多态类型，因此在 Agda 中，上述类型需要是（大！）Π 类型：

这意味着它不在 Set₀ 中：

有没有办法解决这个问题，或者 System F 在这个意义上不能嵌入到 Agda 中？

I'm playing with observational type theory.

Here is equality of π-types (π is the lowercase Π, i.e. π A B is the code for (x : A) -> B x) defined mutually with coercions:

and equality of functions defined accordingly (σ is the lowercase Σ):

So instead of "equal functions map equal inputs to equal outputs" we have "equal functions map definitionally equal inputs to equal outputs".

In this setting coherence

(Univ 0 is Prop, Univ (suc α) is Type α)

is provable. The only thing I needed to postulate is

But we can tweak equality to handle A ≃ A as a special case (I think, trustMe needs a friend _≟_ : ∀ {α} {A : Set α} (x y : A) -> Maybe (x ≡ y)).

We still need to postulate something to define subst and other stuff.

Did I miss something? Do we lose any irrelevance? It seems suspicious to mention type equality in the definition of equality of functions. Do we lose much by restricting inputs of equal functions to be definitionally equal? Is there anything good about having strongly normalizing coherence or it doesn't matter, since it's computationally irrelevant anyway?

The code (I ignored positivity, termination and cumulativity issues altogether).

我一直在阅读Practical Foundations for Programming Languages，发现迭代和同时归纳定义很有趣。我能够很容易地对我在网上找到的偶数和奇数函数的相互递归版本进行编码。

但我不太清楚（我是 F# 新手）是否可以在类型级别而不是通过函数来​​执行此操作。我已经在 F# 中看到了 Peano 数字的实现，所以我觉得这应该是可能的。

（作为一个借口：标题模仿了为什么我们需要单子？）

有容器（和索引的）（和随机的）和描述。但是容器是有问题的，根据我非常小的经验，从容器的角度考虑比从描述的角度考虑更难。非索引容器的类型是同构的Σ——这太不具体了。形状和位置描述有帮助，但在

我们本质上是在使用Σ而不是形状和位置。

容器上的严格正数的自由 monad 的类型有一个相当简单的定义，但Freermonad 的类型对我来说看起来更简单（从某种意义上说，Freermonad 甚至比论文Free中描述的普通 monad更好）。

那么我们可以用比描述或其他东西更好的方式来处理容器吗？

前段时间我读到函数类型a -> b对应于关系a ≤ b，或者是a ≥ b吗？这对我来说很有意义，因为如果我们在它们之间存在双射（即(a ≈ b) ≡ (a -> b, b -> a)），则两种类型是同构的。同样，(a = b) ≡ (a ≤ b) ∧ (a ≥ b)。

我知道这不是 Curry-Howard-Lambek 对应（即类型论、逻辑和范畴论之间的对应）。这是类型论和其他东西之间的对应关系。我想了解更多有关此通信的信息。有人能指出我正确的方向吗？

我知道这似乎不是一个编程问题，但它与编程有关，我希望一些函数式程序员对此有更多了解，并能指出我正确的方向。

为什么我不能像这样定义更明确的异构平等版本：

当我这样做时，我收到以下错误：

我知道这个错误与宇宙层次结构有关，但我不知道具体是什么。它认为Eq T x x应该是Set_1，还是认为是但不应该是？为什么这里有东西Set_1？