Login/Register
What is Haskell's Data.Typeable?
Asked Answered
haskelltypeclassgeneric-programmingscrap-your-boilerplate
B

4

72

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?

Brundage answered 6/7, 2011 at 17:17 Comment(0)
E
47

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.

Elative answered 6/7, 2011 at 23:6 Comment(3)
"the untyped lambda calculus is really the uni-typed lambda calculus" - a beautiful pun! – Delicatessen
Could you explain the difference between an "interpreter" and a "direct representation" in Harper's sense? – Granoff
"The style originated in Abadi et al" -- their paper clearly acknowledges that there were existing implementations of the system they describe before they wrote the paper, dating back to Simula 67, and that their contribution was to provide a formal semantic definition for it. – Goahead
H
17

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.)

Hjerpe answered 6/7, 2011 at 17:33 Comment(3)
No. Typeable does not allow casting, that's in Dynamic. And Dynamic does not allow casting between different types, because it forms a safe wrapper around unsafeCoerce. Typeable fits in as part of Dynamic's safe wrapper. It provides the ability to get a runtime representation of a type. Nothing more. – Kinser
@Carl: cast :: (Typeable a, Typeable b) => a -> Maybe b -- all you need is Typeable, no Dynamic involved! Using Typeable and cast you can in fact roll your own Dynamic fairly easily... – Itacolumite
@sclv, almost, but dynApply and dynApp can't yet be done using the Typeable machinery without unsafeCoerce. That's slated to happen soon, however; Richard Eisenberg, Stephanie Weirich, and a couple other luminaries have been working on it. – Granoff
I
8

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!

Itacolumite answered 6/7, 2011 at 18:58 Comment(0)
A
4

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.

Avebury answered 6/7, 2011 at 17:40 Comment(0)

© 2022 - 2024 — McMap. All rights reserved.