- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

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 Mo Feb 05 2007 - 14:55:01 CET

Date: Mon, 05 Feb 2007 13:51:05 +0100

Hello Wolfgang

* Am 02.02.07 schrieb Wolfgang Lux:

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.

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.

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

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.

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 Mo Feb 05 2007 - 14:55:01 CET

*
This archive was generated by hypermail 2.3.0
: Fr Okt 07 2022 - 07:15:21 CEST
*