Re: casting with a func. pattern

From: Sebastian Hanowski <seha_at_informatik.uni-kiel.de>
Date: Mon, 05 Feb 2007 13:51:05 +0100

Hello Wolfgang


* Am 02.02.07 schrieb Wolfgang Lux:
> Hello Sebastian!
>
> There is no need to use function patterns here. All you need to define
> cast is

You are right. Function patterns aren't essential here. My program
should be equivalent to this one:

        copycast :: Term _ -> Term Empty
        copycast Leaf = Leaf
        copycast (Node l r) = Node (copycast l) (copycast r)

I just liked the function pattern for expressing the fact that a cast
acts only on the type of a piece of data.

> magic' :: _ -> Empty
> magic' = const failed

Sure, in Curry there's no such thing as an empty type. But this
invariant still holds: expressions of type Term Empty which are in
ground, normal form with respect to the metalanguage Curry are ground
with respect to the object language too.
You could safely interprete them over the empty environment.

I admit my definition was misleading. And after reading in the Curry
doc's I'd now write the empty type's eliminator rather like this

        magic :: Empty -> _
        magic = (const unknown $#)

the intuition behind it's signature beeing that, since elements of type
empty are impossible (in ground, normal form...), if you could get one
nonetheless, you probably could get an element of any type you can
imagine.

> cast :: Term _ -> Term Empty
> cast = rename magic'

The renaming maps variables to variables. So you can't get a /closed/
term from an /open/ term by simply renaming it, even if you choose to
rename with an identifier that will never be there. Hence this is an
unsafe cast

>rename (const success) (cast (Var 'x'))
        Var success

To /close/ a term by actually mapping variables you would have to apply
a ground substitution:

        subst :: (a -> Term Empty) -> Term a -> Term Empty

Another possibility to /make/ a closed term would be lambda lifting, if
the object language contained variable binders.

> The only advantage of using function patterns in your example is that
> you can avoid the additional definition of magic' (it wouldn't have
> been necessary if you had omitted the type signature for magic).

Terms built without use of the Var constructor are polymorphic as [],
say. But since terms are non-linear structures a simple case analysis
isn't enough to find out. You need a traversal. Which I had liked to
stuff into a function pattern.


Cheers,
Sebastian




_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mon Feb 05 2007 - 14:55:01 CET

This archive was generated by hypermail 2.3.0 : Mon Sep 23 2019 - 07:15:06 CEST