typesets

4 views
Skip to first unread message

John Skaller2

unread,
May 26, 2022, 5:52:07 AM5/26/22
to felix google
At the moment Felix has a mess arrangement to define typesets:

typedef ints = typesetof (int, long);
typedef floats = typesetof (float, double);
typedef numbers = ints \cup floats; // union

A predicate

T in ints

is reduced to

typematch T with | int -> TRUE | long -> TRUE | _ -> FALSE endmatch

So with a finite set of monomorphic types, it is easy to do all the fun set operations.

However a typeset element could “in principle” be any type pattern so it
represents a whole family of types for example

_ ->_

represents all functions. In this extended interpretation less operations are
available. You’d get overlap too, between say _ * _ and _ ^ 2. Some operations
could be computed with unification. However, some formulas would remain symbolic,
but would render into typematches .. for example the intersection can be computed
by checking for membership in both arguments.

It’s not clear that this complexity is useful.

There is a good reason to stick with finite version: overloading requires
typeset implication. In fact, it decodes typematches to compute implication.
Weirdo. Anyhow consider:

fun g[T in B] (y:B) => ..
fun f[T in A] (x:T) => g[T] (x);

where A, B are typesets. Then the constraint T in A must imply T in B:

(T in A) implies (T in B)

which is easily computed as

A contains B // or A >= B

Felix is bugged in the sense this cannot be done for general constraints.
[In other words, the implication cannot be reduced until after the candidate
is monomorphised, which is too late].




John Skaller
ska...@internode.on.net





Reply all
Reply to author
Forward
0 new messages