Haskell 的 Data.Typeable 是什么?

发布于 11-18 18:46 字数 97 浏览 3 评论 0原文

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

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

I've come across references to Haskell's Data.Typeable, but it's not clear to me why I would want to use it in my code.

What problem does it solve, and how?

如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。

扫码二维码加入Web技术交流群

发布评论

需要 登录 才能够评论, 你可以免费 注册 一个本站的账号。

评论(4

盛装女皇2024-11-25 18:46:07

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

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

该风格起源于 Abadi 等人,并由 Cheney 和 Hinze 为 Haskell 开发,作为表示所有动态类型的包装器,其中 Typeable 类作为 SPJ 和 Lammel 的 SYB 工作的一部分出现。


参考


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

20.4 非类型化意味着统一类型

无类型的 λ 演算可以忠实地嵌入到
具有递归类型的类型化语言。这意味着每个
非类型化 λ 项具有类型化表达式的表示形式
以这样的方式执行一个表示
λ-term 对应于术语本身的执行。这
嵌入不是编写解释器的问题
ℒ{+×⇀µ} 中的 λ 演算(我们肯定可以做到),但是
而是将非类型化 λ 项直接表示为类型化
具有递归类型的语言中的表达式。

关键的观察结果是非类型化 λ 演算是
确实是单类型 λ 演算!这不是缺席
赋予它力量的类型,而是它拥有
只有一种类型,即递归类型

D = µt.t → t。

Data.Typeable is an encoding of an well known approach (see e.g. Harper) to implementing delayed (dynamic) type checking in a statically typed language -- using a universal type.

Such a type wraps code for which type checking would not succeed until a later phase. Rather than reject the program as ill-typed, the compiler passes it on for runtime checking.

The style originated in Abadi et al., and developed for Haskell by Cheney and Hinze as a wrapper to represent all dynamic types, with the Typeable class appearing as part of the SYB work of SPJ and Lammel.


Reference


Even in the text books: dynamic types (with typeable representations) are statically typed languages with only one type, 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.

很快妥协2024-11-25 18:46:07

它是一个允许命名类型等功能的库。如果类型 a 被声明为 Typeable,那么您可以使用 show $ typeOf x 获取其名称,其中 xa 类型的任何值。它还具有 有限的类型转换

(这有点类似于C++的RTTI或动态语言的反射。)

It's a library that allows, among other things, naming types. If a type a is declared Typeable, then you can get its name using show $ typeOf x where x is any value of type a. It also features limited type-casting.

(This is somewhat similar to C++'s RTTI or dynamic languages' reflection.)

诗化ㄋ丶相逢2024-11-25 18:46:07

我能找到的最早的 Haskell 类 Data.Typeable 库的描述之一是 John Peterson 在 1992 年所做的: http://www.cs.yale.edu/publications/techreports/tr1022.pdf

我所知道的最早介绍实际情况的“官方”论文Data.Typeable 库是 2003 年第一篇 Scrap Your Boilerplate 论文:http://research.microsoft.com/en-us/um/people/simonpj/Papers/hmap/index.htm

我确信有很多干预历史,有人这里可以插话!

One of the earliest descriptions I could find of a Data.Typeable-like library for Haskell is by John Peterson from 1992: http://www.cs.yale.edu/publications/techreports/tr1022.pdf

The earliest "official" paper I know of introducing the actual Data.Typeable library is the first Scrap Your Boilerplate paper from 2003: http://research.microsoft.com/en-us/um/people/simonpj/Papers/hmap/index.htm

I'm sure there's lots of intervening history that someone here can chime in with!

锦爱2024-11-25 18:46:07

使用 Data.Typeable 类主要用于 废弃您的样板 (SYB) 风格。

另请参阅 Data.Data SYB定义了一个集合组合器,用于在各种用户创建的类型上以统一的方式执行打印、计数、搜索、替换等操作。 Typeable 类型类提供了必要的管道。

在现代 GHC 中,您可以在定义自己的类型时直接说deriving Data.Typeable,以便为其提供必要的实例。

The Data.Typeable class is used primarily for generic programming in the Scrap Your Boilerplate (SYB) style. See also Data.Data

The idea is that SYB defines a collection combinators for performing operations such as printing, counting, searching, substiting, etc in a uniform manner over a variety of user-created types. The Typeable typeclass provides the necessary plumbing.

In modern GHC, you can just say deriving Data.Typeable when defining your own type in order to provide it with the necessary instances.

~没有更多了~
我们使用 Cookies 和其他技术来定制您的体验包括您的登录状态等。通过阅读我们的 隐私政策 了解更多相关信息。 单击 接受 或继续使用网站,即表示您同意使用 Cookies 和您的相关数据。
原文