from static typing to runtime constraints

From: Sebastian Hanowski <seha_at_informatik.uni-kiel.de>
Date: Fri, 08 Dec 2006 07:55:40 +0100

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 Fri Dec 08 2006 - 09:27:42 CET

This archive was generated by hypermail 2.3.0 : Mon Sep 16 2019 - 07:15:05 CEST