This message illustrates how safe casting with multiple universes can
be extended to new user-defined, polymorphic datatypes. We show a
_portable_ mapping of polymorphic types to integers. Different
instances of a polymorphic type map to different integers. Phantom
types can be either disregarded or accounted for -- as the user
wishes. Furthermore, if two different applications running on two
different machines agree on the same type heap, then they agree on the
type encoding. An application can use multiple typeheaps at the same
time. It is easy therefore to dedicate one particular typeheap for
portable encoding of types across several computers.
Incidentally, our encoding of types may take into account _values_ of
some of the components of a polymorphic type. For example, given a
value of a type 'Foo Int a', the encoding may use the _value_ of the
first component and the _type_ of the second component. When we do the
cast, we can check not only for the desired type but also for the
desired values. We can thus approach dependent types.
This message hopefully replies to Ralf Laemmel's comment:
] You should make very clear that there is
] not just a single safeCoerce, but the TI/init_typeseq argument has to
] be constructed and supplied by the programmer in a way that (s)he
] decides what array of types can be handled. So if you wanted to use
] your approach to scrap boilerplate [1], say deal with many datatypes,
] this becomes quite a burden. Think of actually building initial type
] sequences. Think of how combinators need to be parameterised to take
] type sequences.
with which I agree. Below I try to make it very implicit what depends
on TI/init_typeseq and what doesn't, and how much work is involved in
adding new datatypes and extending type heaps. I don't know if the
proposed approach is better than the others in many
circumstances. It's certainly different.
Ralf Laemmel also wrote:
] Software-engineering-wise your approach suffers from an important
] weakness: a closed world assumption. The programmer has to maintain
] your TI and pass it on in all kinds of contexts for the array of
] types to be handled.
I thought it is a feature. I thought a programmer can import some type
heap, partially apply the needed function to it, and re-export the
latter. The example below demonstrates what is involved when a new
datatype is added. It seems not that much.
] I didn't need undecidable not even overlapping instances.
I don't actually need overlapping-instances extensions. An earlier
message on the subject of MRefs used similar type heaps without any
need for -fallow-overlapping-instances. However I had to use numeral
types such as Succ (Succ ... Zero) rather than Int for type
indices. The current approach looks more elegant. Besides, you seem to
in favor of giving overlapping instances more acceptance, support and
legitimacy.
] Is it obvious to see that fetching stuff from the type sequences would
] be indeed efficient for long PLists?
The sequence of 'cdr' operations needed for fetching stuff is known
statically. A compiler might therefore do something intelligent.
This whole message is self-contained, and can be loaded as it is in
GHCi, given the flags
-fglasgow-exts -fallow-undecidable-instances -fallow-overlapping-instances
We start with the boilerplate, which has changed a little (for
example, the class PLists now has a member function pllen).
data Nil t r = Nil
data Cons t r = Cons t r
class PList ntype vtype cdrtype where
cdr:: ntype vtype cdrtype - cdrtype
empty:: ntype vtype cdrtype - Bool
value:: ntype vtype cdrtype - vtype
pllen:: ntype vtype cdrtype - Int
instance PList Nil vtype cdrtype where
empty = const True
pllen = const 0
instance (PList n v r) = PList Cons v' (n v r) where
empty = const False
value (Cons v r) = v
cdr (Cons v r) = r
pllen (Cons v r) = 1 + pllen r
class TypeSeq t s where
type_index:: t - s - Int
fetch:: t - s - t
alter:: t - s - s
instance (PList Cons t r) = TypeSeq t (Cons t r) where
type_index _ _ = 0
fetch _ (Cons v _) = v
alter newv (Cons v r) = Cons newv r
instance (PList Cons t' r', TypeSeq t r') = TypeSeq t (Cons t' r') where
type_index v s = 1 + (type_index v $ cdr s)
fetch v s = fetch v $ cdr s
alter newv (Cons v' r') = Cons v' $ alter newv r'
The initial typesequence:
init_typeseq = Cons (undefined::Char) $
Cons (undefined::Int) $
Cons (undefined::Bool) $
Cons (undefined::String) $
(Nil::Nil () ())
and its type. See the previous message for more discussion of the
latter.
type TI
= (Cons
Char
(Cons Int (Cons Bool (Cons String (Nil () ())
Because we will be dealing with existential types, we need to extend
the compile-time indexing into run-time:
class (TypeSeq t u) = TypeRep t u where
tr_index:: t - u - Int
tr_index =
