Hello
I had liked to share an example where hiding a complex traversal
operation in a /function pattern/ gives a descriptive notion.
Given a representation of expressions as an inductive datatype
parameterised in the type of variables
data Term a = Var a | Leaf | Node (Term a) (Term a)
and a notion of the empty set
data Empty
one gains a /static/ description of /closed/ expressions: Term Empty
Elements of this type can't have been made using the constructor Var,
because arguments to it are absent from the program.
(In Curry one can still have Var unknown::Term Empty, I'll address this
later.)
It could be nice to be able to cast variable-free terms built over an
arbitrary type to closed terms, i.e. cast :: Term _ -> Term Empty
We have that:
- The empty type comes with an 'eliminator' as any other type, replacing
'constructors' like for example foldr does with nil and cons for lists.
magic :: Empty -> _
magic = \_ -> failed
- We can rename terms. Which corresponds to functorial mapping for this
datatype. (Compare the signature with the one for map for lists.)
rename :: (a -> b) -> Term a -> Term b
rename f (Var x) = Var (f x)
rename _ Leaf = Leaf
rename f (Node s t) = Node (rename f s) (rename f t)
(A typical example of a renaming is for example
>:t rename ord
rename ord :: Term Char -> Term Int
turning variables made from characters into their ASCII values.)
Now, following McBride in mapping the empty type's eliminator across
functorial datastructures
http://sneezy.cs.nott.ac.uk/containers/blog/?p=31
inflate :: Term Empty -> Term _
inflate = \t -> rename magic t
I was wondering wether this gives a suitable notion of a cast to closed
terms:
cast :: Term _ -> Term Empty
cast (inflate t) = t
This program expresses that closed terms are exactly those arbitrarily
typed terms which could be viewed as suitably renamed terms over the
empty variable set.
Please observe that this program rightly computes no solution for:
! > cast (Var unknown)
And that it does so without any additional testing for free variables
(of the host language Curry).
Attempts to unsafe casts by inhabiting the empty set with the divergent
element
! > cast (Var bottom)
get mapped to finite failure too.
And after you've convinced the typechecker that your term eventually
given already a ground type is in fact a polymorphic object because it
makes no reference to the type parameter, you can safely cast it further
to a term over any other type you like.
You will just have to inflate it once again.
Cheers,
Sebastian
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Feb 02 2007 - 12:08:10 CET