Hi all,
Sergio Antoy once pointed out the correspondence between a datatype
declaration like
data Color = Red | Green
and a 'generator' for that type
Color = Red ? Green
such that typing a free variable
x :: Color
would result in constraining it with the generator
x =:= Color
This scheme is only viable for first-order data and care has to be
taken when exploring it beyond enumeration types.
Curry uses variable sharing to avoid the repeated evaluation of
expressions duplicated by call-by-name beta-reductions. And even in a
call-by-name language this leads to a call-time-choice semantics of
non-determinism.
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.
On the other hand hardwiring parameter signatures with encodings of
specific instances of parameterized types like
data TreeColor = Leaf | Node Color TreeColor TreeColor
TreeColor = Leaf ? Node Color TreeColor TreeColor
neglects the fact that constructors like Tree are type-indexed families
of (inductive) types.
But the recent extension of Curry with /function patterns/ introduced
variables which are bound to unevaluated expressions when defined
functions are applied to them in pattern expressions on the left-hand
side. One can thus exploit run-time-choice non-determinism for the
encoding of type constructors.
Tree (id a) = Leaf ? Node a (Tree a) (Tree a)
> Node Red (Node Green Leaf Leaf) Leaf =:= Tree Color
It may look contrived to have notions for verifying static properties
of programs available at runtime. But since type signatures are optional
it would nice if writing them down would be rewarding.
Best regards,
Sebastian
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Dez 08 2006 - 09:27:42 CET