Feature request: GeneralizedTypes, TypedFunctions, type checking, and more
Nobody has claimed this yet.
- Dominant language
- Macaulay2
- Stars
- 435
- Forks
- 297
- Avg merge
- 4d 20h
- Merged PRs (30d)
- 11
Description
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:
```m2
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:
```m2
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:
```m2
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:
```m2
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
```m2
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:
```m2
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:
```m2
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:
```m2
(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.:
```m2
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.
```m2
signature(f : Function) := FunctionSignature : ( ... )
```
This should also allow getting the type of a `TypedSymbol`:
```m2
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:
```m2
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.
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
No source files, tests, or entry points are identified. Start by mapping the existing method, function, type, lookup, and instance implementations, then narrow the proposal to a documented first milestone with tests; completion is not defined for the full set of requested features.
Written by the indexing model from the issue text.
Assessment
- Domain
- compilers
- Issue type
- Feature
- Difficulty
- 5/5
- Estimated time
- Over a week
- Activity status
- Stale
- Clarity
- Needs clarification
- Newbie friendliness
- 15/100