Re: Extensible downcasts impossible in Haskell? (was Re: Monomorphism, monomorphism...)
Tue, 9 Oct 2001 10:50:19 +1300, Tom Pledger <Tom.Pledger@peace.com> pisze:
I'm curious about this impossibility.
- Is it well known? If so, would someone please refer me to a paper or posting which explains it?
I don't know. I'm not even sure if some clever encoding couldn't express it, but I can't imagine how it could do it and I would guess that it's impossible. It's not easy to formulate the question precisely but I'm quite sure that it's a well defined problem. You want to be able to embed arbitrary Haskell types in "subtypes". So it doesn't suffice to make a universal type with many useful concrete types under constructors, which emulates dynamically typed languages with a fixed number of types like Lisp or Erlang (I think). Because an interface of abstract types not included in this set may have binary methods or alike, so you can't just wrap the interface in a tuple of functions with types taken from the included set only.
- Does it just affect Haskell 98, or does it have deep implications for any future language extensions?
IMHO it's independent from most extensions. The only extension I know of which could be used for implementing downcasts is Dynamic. Some extensible algebraic types (where definition of constructors is spread among an open set of modules) would allow downcasts too I think.
- How does it relate to the alternative record mechanism idea you mentioned a while ago?
http://haskell.org/pipermail/haskell/2000-December/000213.html
My mechanism doesn't allow downcasts, although it promotes a style of programming which probably wants to use downcasts sometimes. It's described as a translation to Haskell 98 with multiparameter classes, fundeps, the ability to gather label names from all modules and associate each name with an unique class, and some small adjustments of the type system (related to the termination of typechecking). These extensions don't provide anything useful for implementing downcasting, so I couldn't implement downcasts without changing the compiler even if I specified them somehow. -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK
Thanks for the further explanation, Marcin. If I understand correctly, you're talking about explicitly named algebraic types, not just unions where the type is an anonymous reflection of the structure as in: Var (foo :: Int, bar :: Char) -- in the style of "A Polymorphic Type System for Extensible -- Records and Variants" (Gaster & Jones) and: Either Int (Either Char ()) -- in the extensible union type mechanism of "Monad Transformers -- and Modular Interpreters" (Liang, Hudak & Jones) I've sometimes wondered whether it would be appropriate to implement the summing aspect of `data' by wrapping `newtype' around such extensible variants. (There'd still need to be some construct for the other aspects of `data': products and strictness flags.) For example, this: data T a b = T1 a !Int | T2 b could translate to something like this: newtype T a b = T {unT :: Var (t1 :: (a, !Int), t2 :: b)} Then there'd be a way to extract a value of a structurally named type from a value of an explicitly named type. Would this help to combine explicitly named types with add-a-field subtyping and remove-a-summand subtyping? For that matter, is it how O'Hugs already works beneath the surface? Regards, Tom
participants (2)
-
Marcin 'Qrczak' Kowalczyk -
Tom Pledger