disco-lang / disco

Functional teaching language for use in a discrete mathematics course
Other
162 stars 23 forks source link

Make count and enumerate work for user-defined recursive types #175

Open byorgey opened 5 years ago

byorgey commented 5 years ago

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.

byorgey commented 3 years ago

Actually, should be easy now with the enumeration library!

byorgey commented 2 years ago

This seems important to be able to do things like define recursive trees and enumerate or count them.

byorgey commented 2 years ago

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
byorgey commented 7 months ago

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:

  1. 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 time VType values are created.
  2. 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?)