It is now possible to write type constraints like this:
-----------------------------------------
fun ff[t,k where t==k ]: t * k -> t = "$1+$2";
print$ ff$ 1,2;
print$ ff$ 1,2.0; // should fail
------------------------------------------------
The first case passes because int == int,
the second fails because int != double.
A constraint is any type expression. If it reduces
to 0 (void), the constraint fails. If it reduces
to 1 (unit), the constraint passes.
If it fails to reduce, you will currently get an error.
It's possible this should be treated in some cases
as a failure (not sure).
The 'where' constraints currently do NOT contribute
to type variable deduction (mainly because I'm lazy).
The module Typing is now open and contains the following
useful operators:
prefix infix meaning
-------------------------
eq == equality
land and logical and
lor or logical or
dom domain of a function
cod codomain of a function
prj1 first component of a pair
prj2 second component of a pair
All these operators are defined using the typematch feature.
The following features are also available and provided by the
desugaring pass and the core type system:
compl ~ categorical dual
proj_<n> n'th projection of a tuple (codomain of)
_isin _isin (elt,typeset)
_case_arg_<n> n'th injection of a sum (domain of)
and of course the usual typematch and lamdba expressions.
Typesets are created like:
typesetof(int,long, float)
and can be combined with infix || (union) and && (intersection)
operators.
At present the family of operations is somewhat adhoc.
Note the type system supports intersection types natively
but there's no notation for it!
The following should hold:
_isin (t,typesetof(y)) ==
typematch t with | y => 1 | _ => 0 endmatch
but probably doesn't work. This is basically an encoding
of the logic/set theory isomorphism
P(x) == x in { x | P(x) }
The biggest problem, however, is that there is no 'tail'
and 'cons' operator for tuples such that
t == cons (proj_n t, tail t) // where t is a tuple type
I will add this, since it is necessary for recursive analysis
of tuples using typematches. A similar pair of operators is
required to analyse sum types, although it can be done
immediately using the categorical dual.
Most interestingly .. we'd like to GET RID of these operators
by using polyadic programming. In particular 'cons' and
its dual are just two iterable type constructors. Another
one is function formation: here are the three listed:
a * b * c * ...
a + b + c + ...
a -> b -> c -> ...
but we'd really like:
a * b * c * .. = fold * (a, b, c ..)
a + b + c * .. = fold + (a, b, c ..)
a -> b -> c .. = fold -> (a, b, c .. )
That is, we'd REALLY like to treat tuple, sum, and function
type constructors as ordinary type functions we can fold
over a type tuple.
Since typematch has been modified to conform to Barry Jays maxim
"every expression is a pattern", we should be able to achieve
recursive type analysis of such data types generically with
pattern matching.
For example you should be able to say
all the components of the tuple are fast integers
using 'filter', which in turn is encoded by recursive
desconstruction of a folded data type encoding.
One of the key difficulties here is that tuples and sums
aren't associative, so that a tuple or sum type is NOT
built inductively (note that -> is left associative).
This basically requires a way to deconstruct a tuple
or sum type into a type tuple, and the operators
head, tail, cons
for type tuples. With some thought we should obtain
fully polyadic system! (This is the Holy Grail)
Hmm .. I'm seeing how to do this now!
Anyhow, we need the 'where' clause and 'specialisations'
to implement typeclasses.
--
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net
-------------------------------------------------------------------------
Take Surveys. Earn Cash. Influence the Future of IT
Join SourceForge.net's Techsay panel and you'll get the chance to share your
opinions on IT & business topics through brief surveys -- and earn cash
http://www.techsay.com/default.php?page=join.php&p=sourceforge&CID=DEVDEV
_______________________________________________
Felix-language mailing list
Felix-language@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/felix-language
