What can Extensions
type args be used for?
#718
Replies: 3 comments
-
The intention was to be able to define something like So in fact I think we should be able to do all the things you mention: use it in Lift nodes, use it in function types (where it makes sense, e.g. as the delta) , and use it as the concrete (input-)resources of a node (within the scope of that binder). When you say we can't do that at the moment, have you tried **the issue that |
Beta Was this translation helpful? Give feedback.
-
@croyzor is there more TBD here or can we close this? Are there specific tasks that need adding? (fwiw I think "generalize Lift to an ExtensionSet" is simple enough and useful enough to be worth doing even if the long-term goal is to remove Lift nodes altogether.) |
Beta Was this translation helpful? Give feedback.
-
We can close this, but I'll open up "generalise lift nodes to extensionset" as an issue |
Beta Was this translation helpful? Give feedback.
-
In our kinds of type parameters, we allow "Extensions", which is the type of sets of extensions. However, the things that we can do with this at the moment are quite limited. Is that a bug or a feature?
If I define a
PolyFuncType
which takesTypeArg
s which check against[TypeParam::Extension]
then I can create the typeT = (TypeEnum::Variable(0, bound), bound)
. Note: the "bound" arguments don't make much sense here, but let's forget about that for now.What can I now do with this type
T
? It seems all I can do is pass it to the nextPolyFuncType
I want to use as aTypeArg
. I can use it as an input/output in function signatures, but then it would be ill-kinded and (hopefully!) fail validation. Currently, neither theextension_delta
of aFunctionType
, nor theinput_extensions
of aSignature
will accept thisType
in place of a concreteExtensionSet
.This is good for correctness, at the cost of expressibility.
So what can we do with this
TypeArg
?PolyFuncType
scompute_signature
methodWhat can't we do:
What do we want to be the case?
Beta Was this translation helpful? Give feedback.
All reactions