Go up to Top
Go forward to 2 Proposals for changes to the syntax
1 Introduction
We would like to extend CASL to allow
- declaration of higher-order functions and predicates
- formation of terms of higher-order functional types
(i.e. formation of terms denoting functions)
For instance, it should be possible to
declare a function like
twice : (int -> int) -> (int -> int),
where int is a (basic) sort declared in a sort declaration,
and it should be possible to write a term of type
int -> int like twice(f),
where f is another term of type int -> int.
This gives rise to two major questions:
- which changes to the syntax do we want, and
- how can we give static and dynamic semantics to the extended language
In the following, we will discuss possible answers to these questions,
with emphasis on issues related to subtyping.
We will use the term basic sort for a sort
declared in a sort declaration, and the term
type for a basic sort or a functional type.
As concrete syntax for the total and the partial function type constructors
we will use -> and +, respectively.
CoFI
Note: L-2 --Version 1.0-- 10 April 1997.
Comments to ah@it.dtu.dk