I have a recursive algebraic datatype. I (somewhat arbitrarily) defined one function to compute distance between instances, and am trying to define a function to approximate a "vector" between instances. I assume there's no single way to define a metric space on top of a definition of an algebraic data type, much less a vector space, but was wondering what literature exists about treating recursive algebraic datatypes as existing in a topological space with meaningful comparisons.

The reason I want to treat it like a vector space is because I want to define interpolation between two structures in some reasonable manner.

  • $\begingroup$ What do you need these structures for? That might direct possible choices in a useful way. They yearning for vectors makes it look like you're secretly doing machine learning. $\endgroup$ – Andrej Bauer Jul 31 '18 at 13:48
  • $\begingroup$ Haha, I do come from something of a machine learning background, so maybe that shows through! $\endgroup$ – lightning Jul 31 '18 at 16:56

It is possible to construct recursive datatypes (algebraic datatypes are a special case) in a suitable category of complete metric spaces, see for instance P. America and J. Rutten's Solving Reflexive Domain Equations in a Category of Complete Metric Spaces, Journal of Computer and System Sciences 39, 343-375 (1989).

As for making vector spaces out of algebraic datatypes, I do not really know, but if you explain what you want them for, we might be able to suggest something.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.