Feature request: GeneralizedTypes, TypedFunctions, type checking, and more

[mahrud]

When declaring the method, TypicalValue => Type can be used to specify the return type of the output. Alternatively, when installing methods, one can specify the return type:

length List := ZZ => L -> ...

However, this is not possible for function closures because the return type is a feature of methods, not an internal property of functions.

My proposal is to introduce various new classes for generalized types and typed functions which have intrinsic input and return types. This supersedes #1375, and will be eventually used for type checking functions.

Here is my suggestion for the syntax:

foo =  List : L          ->  ZZ      : ( ... ) -- takes a list, returns an integer
bar = (List : L, ZZ : n) ->  ZZ      : ( ... ) -- takes a list and an integer, returns an integer
blah =           ZZ : n  -> (ZZ, ZZ) : ( ... ) -- takes an integer, returns a pair of integers

-- takes an integer a, returns a function with signature ZZ : b -> ZZ : ( ... )
foo = ZZ : a -> ZZ : b -> ZZ : ( ... )

-- takes an integer and returns an integer, with an integer as optional value
bar = { ZZ : Strategy => 12 } >> opts -> ZZ : n -> ZZ : ( ... )

Note that for normal functions (i.e. not methods), there's no need to do a lookup. It suffices to check the input types (and ideally also output types).

Ideally, such functions should have a new type, like TypedFunction or TypedFunctionClosure.

Possible extensions:

Improve the notation for installing a method

If the suggestion above is adopted, we can still install a typed function closure on a method like this:

foo' = (ZZ : n, QQ : r) -> List : ( .. )
foo(ZZ, QQ) := foo'

But it would be nice to also accept this for installing a method for uniformity:

foo(ZZ : n, QQ : r) := List : ( ... )

I thought about whether I prefer := there or ->, but I think := makes more sense.

Improve NewMethod and friends

See #1690, combine it with generalized types.

TypedSymbol

This is a convenient notation to assign to Type : Symbol, which can return either a simple list, similar to an Option, or as a new internal class TypedSymbol. In that case, assignment to a TypedSymbol should type check the new value as well.

ListType for lists and sequences of prescribed type

foo = ZZ : n -> Sequence : S -- a sequence of arbitrary size and type
foo = ZZ : n ->   List   : L -- a list of arbitrary size and type
foo = ZZ : n ->  (4:ZZ)  : S -- a sequene 4 integers
foo = ZZ : n ->  {4:ZZ}  : L -- a list 4 integers
foo = ZZ : n -> (ZZ..ZZ) : S -- a sequence of arbitrarily many integers
foo = ZZ : n -> {ZZ..ZZ} : L -- a list of arbitrarily many integers

This is tangentially related to #1978, but we would need to also introduce Type..Type, which I think should give a special object of type ListType. This type may also support lists or sequences of varying types:

foo = ZZ : n -> {ZZ,QQ} : L -- a list of an integer and a rational
foo = ZZ : n -> {ZZ,4:QQ} : L -- a list of an integer and a 4 rationals
foo = ZZ : n -> {ZZ,QQ..QQ} : L -- a list of an integer and arbitrarily many rationals

UnionType for symbols that can have multiple types

If a function may take in or return different types in different cases, one option is to assign the first common ancestor of the possible types, which may simply be Thing, but we can also introduce a new type UnionType which is constructed using Type | Type and can be used like this:

foo = (ZZ | QQ) : n -> (ZZ | QQ) : ( ... ) -- either an integer or a rational

GeneralizedType for recursive type definitions

It should be possible to combine all of the above into things like this:

 (2 : (ZZ | QQ | RR)) -- a pair of reals, rationals, or integers
((2 : (ZZ | QQ | RR)) | CC) -- either as above, or a complex number
{(2 : (ZZ | QQ | RR)) | CC .. (2 : (ZZ | RR)) | CC} -- an arbitrary length list of the above

FunctionSignature for the type signature of a function

Objects of this class would store the input types, and return types of a function, each as a GeneralizedType. It's convenient to have a designated type for this so it can be pretty printed, e.g.:

i1 : toString foo

o1 : foo : (ZZ : n, QQ : r) -> ZZ -- or even ZZ ✕ QQ -> ZZ

Along with this comes a signature method for getting the signature object, which can eventually be used to check whether two or more functions can be composed without running them.

signature(f : Function) := FunctionSignature : ( ... )

This should also allow getting the type of a TypedSymbol:

signature(S : TypedSymbol) := GeneralizedType : ( ... )

A generalized instance method for type checking

For checking whether a given object satisfies the input or return type of a function, defined as above:

instance(x : Thing, T : GeneralizedType) := Boolean : ( ... )
instance(f : Function, S : FunctionSignature) := Boolean : ( ... )

This is the reason we define TypeList and UnionType instead of directly jumping to GeneralizedType, so that implementation of instance becomes easier. In particular, instance(Thing, UnionType) and instance(Thing, ListType) are pieces of cake to implement, and from there GeneralizedType is an easily implemented breath-first or depth-first search. Similarly, the function signature checking syntax is just doing the same twice with the domain and codomain of the function.

Note that a TypedSymbol doesn't need to be this complicated, but it may accept a generalized type as well, I think that's reasonable.

Tangentially related: I really wish instance_Type Thing worked, which would allow something simple like all(L, instance_Type), but I'm reluctantly okay with all(L, instance^Type), as is suggested in https://github.com/Macaulay2/M2/issues/1630#issuecomment-735361979.

A simplified lookup method

List types can be used to significantly simplify lookup, because each method would be installed on precisely one ListType object which may be garbage collected sooner than each of the individual types in it. The downside would be that going up the inheritance tree would be more complicated and potentially slower, but that may be worth it. For now, we can limit the input type of methods to be the way they currently are.

Many other functions would need to also be improved (e.g. lookup, methods #1331, etc.), but perhaps those can wait for their own issue.

[mahrud]

A very useful aspect of the union type idea above is to simplify the situation when you enter methods basis and you're hit with a whopping 43 items, when it really needs to be 8 or 12 at most if we could combine a bunch of them into (basis, Degree, Module) where Degree can be any of ZZ, List, InfiniteNumber. The same is true about declaring all those methods.

[mahrud]

Another useful addition are abstract types and subtypes. For instance, I'd like to define functions:

foo1 Ideal             := I -> (...)
foo2 Ideal::LeftIdeal  := I -> (...)
foo3 Ideal::RightIdeal := I -> (...)

In such a way that foo1 works for any type of ideal (e.g. get the ring), foo2 works only for left ideals, and foo3 works only for right ideals. Here Ideal is an umbrella for both, so it does not inherit from either, and in particular LeftIdeal and RightIdeal could inherit from different types! e.g. LeftIdeal could inherit from hash tables and RightIdeal could inherit from mutable hash tables, and they would both be subtypes of the abstract type Ideal, which may inherit from something else entirely.