haskell - Haskell 的 Data.Typeable 是什么？

Question

我遇到过对 Haskell 的 Data.Typeable 的引用，但我不清楚为什么要在代码中使用它。

它解决了什么问题以及如何解决？

Answer 1

Data.Typeable 是一种众所周知的方法(参见 Harper)的编码，用于在静态类型语言中实现延迟(动态)类型检查 - 使用通用 类型。

这样的类型包装了类型检查直到稍后阶段才会成功的代码。编译器不会将程序作为错误类型而拒绝，而是将其传递给运行时检查。

这种风格起源于 Abadi 等人，由 Cheney 和 Hinze 为 Haskell 开发，作为表示所有动态类型的包装器，Typeable 类作为 SPJ 和 SYB 工作的一部分出现拉梅尔。

<小时/>

引用

• Martín Abadi、Luca Cardelli、Benjamin Pierce 和 Gordon Plotkin，“Dynamic Typing in a Statically Typed Language”，ACM 编程语言和系统汇刊 (TOPLAS)，1991 年。
• James Cheney 和 Ralf Hinze，“A lightweight implementation of generics and dynamics”，Haskell '02:2002 年 ACM SIGPLAN Haskell 研讨会论文集，2002 年。
• Lammel、Ralf 和 Jones、Simon Peyton，“Scrap your boilerplate: a practical design pattern for generic 编程，TLDI '03:2003 年 ACM SIGPLAN 国际语言设计和实现类型研讨会论文集，2003 年
• Harper，2011 年，编程语言实用基础。

<小时/>

即使在教科书中:动态类型(具有可类型表示)也是只有一种类型的静态类型语言，Harper ch 20:

20.4 Untyped Means Uni-Typed

The untyped λ-calculus may be faithfully embedded in a typed language with recursive types. This means that every untyped λ-term has a representation as a typed expression in such a way that execution of the representation of a λ-term corresponds to execution of the term itself. This embedding is not a matter of writing an interpreter for the λ-calculus in ℒ{+×⇀µ} (which we could surely do), but rather a direct representation of untyped λ-terms as typed expressions in a language with recursive types.

The key observation is that the untyped λ-calculus is really the uni-typed λ-calculus! It is not the absence of types that gives it its power, but rather that it has only one type, namely the recursive type

D = µt.t → t.