disco
disco copied to clipboard
Make count and enumerate work for user-defined recursive types
Original comment: Have to extend count and enumerate to take the context of type definitions. Count has to do some kind of least fixed point computation, or a Jacobian matrix or something like that...
Using the enumeration
library, and the fact that we should no longer support enumeration of infinite types (because lists are strict and hence finite), this should not be too bad. See also #309 and #347.
Actually, should be easy now with the enumeration library!
This seems important to be able to do things like define recursive trees and enumerate or count them.
Note that at the moment we can actually make Disco crash:
Disco> type X = Unit + Unit + Unit
Disco> count(X)
left(■)
Disco> enumerate(X)
disco: enumType: can't enumerate TyCon (CUser "X") []
CallStack (from HasCallStack):
error, called at src/Disco/Enumerate.hs:174:23 in disco-0.1.5-58eEULBwaXh4U3Jv7xOL2y:Disco.Enumerate
See https://github.com/disco-lang/disco/blob/474384f5682dcd2b94f0aae1a58c578f1639c6df/src/Disco/Enumerate.hs . The obvious thing we need to do is extend the enumType
function to handle TyUser
. However, in order to do that we would need to add an extra argument to enumType
, enumTypes
, enumerateType
, and enumerateTypes
, namely, a map from user-defined type names to their definitions; however, that map is not available at runtime. Some solutions that come to mind:
- Perhaps
VType
values should also contain the mapping from user type names to definitions. I don't know how easy/possible it would be to capture that map at the timeVType
values are created. - We could transform type values into a closed form using fixpoint bindings.
In any case, the idea would be build a lazy map from type names to enumerations; when we see a name that is already in the map we can stick an infinite
combinator on top of the looked-up enumeration to prevent unproductive recursion. (Possible problem: do we need to do some analysis in order to only insert infinite
when the type is, in fact, infinite?)