Re: from static typing to runtime constraints

From: Bernd Brassel <bbr_at_informatik.uni-kiel.de>
Date: Fri, 08 Dec 2006 13:24:51 +0100

Sebastian Hanowski wrote:
Hi Sebastian,

thanks for the input!

> While this is the desired behaviour in certain cases, like for example
> when using an instance of the type of Integers in a let-binding to
> generate even numbers as Antoy/Hanus observe in their ICLP 2006 paper,
> it at the same time disables a straightforward encoding of /type
> constructors/
>
> data Tree a = Leaf | Node a (Tree a) (Tree a)
>
> Tree a = Leaf ? Node a (Tree a) (Tree a)
>
> ! > Node Red (Node Green Leaf Leaf) Leaf =:= Tree Color
>
> because a 'type parameter' can't evaluate to different instances on the
> right-hand side.

In order to code this, I would use the old Haskell trick to "transform"
variables into functions:

type Generator a = () -> a

Tree :: Generator a -> Generator (Tree a)
Tree a _ = Leaf ? Node (a ()) (Tree a ()) (Tree a ())

But your trick is really cool. But I wonder if this behavior is really
intended by the semantics of function patterns.


Thanks for the thought provoking example!
Bernd

_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Dez 08 2006 - 13:47:08 CET

This archive was generated by hypermail 2.3.0 : Do Jun 20 2024 - 07:15:08 CEST