Encoding Any type
Representing Any type as \sigma* is expensive (where \signma is the
union of all literals) for implementation relied on structured
representation.
To solve this problem, we exploit existential type.
First we define a Regtype for Any
data ANY = ANY
and a run time structured representation for ANY
data Any = forall r h ([[r]] = h). K r h
We know
r \leq_d^u Any
out of this we derive,
u :: r -> ANY -> h -> Any
u r _ h = K r h
d :: ANY -> r -> Any -> Maybe h
d _ r (K (r' h)) = d r' r h
This won't work. The reason is as follows. First the instance for d r' r h might not exist, in that case Nothing must replace it. Second, this needs to be checked at runtime.
To solve this problem, we exploit existential type.
First we define a Regtype for Any
data ANY = ANY
and a run time structured representation for ANY
data Any = forall r h ([[r]] = h). K r h
We know
r \leq_d^u Any
out of this we derive,
u :: r -> ANY -> h -> Any
u r _ h = K r h
d :: ANY -> r -> Any -> Maybe h
d _ r (K (r' h)) = d r' r h
This won't work. The reason is as follows. First the instance for d r' r h might not exist, in that case Nothing must replace it. Second, this needs to be checked at runtime.
