TODO List - Githubissues

Drup / dowsing

᚛ A type of divination employed in attempts to locate identifiers matching a given type expression

ISC License

35 stars 4 forks source link

TODO List #3

Open Drup opened 3 years ago

Drup commented 3 years ago

Software engineering

[x] Add tests
[x] Implement a proper notion of printing environment
[x] Use proper logging
[x] Plug together the unification and the database again

Science

[ ] Make sure the returned unifiers are minimal
[x] Add rigid variables

Indexation:

[x] Head
[x] Nb of arguments ("Equal" or "At least")
[ ] Variances of constants
[ ] Term indexing: To Read:
- http://wwwlehre.dhbw-stuttgart.de/~sschulz/PAPERS/Schulz2013-FVI.pdf
- Fingerprint Indexing for Paramodulation and Rewriting

Drup commented 2 years ago

Reading list and/or references

[RDC]: Di Cosmo (Roberto). - Isomorphisms of types: from lambda-calculus to information retrieval and language design. - Birkhauser, 1994.
[Rit90] Mikael Rittri. Retrieving library identifiers by equational matching of types in 10th Int. Conf. on Automated Deduction. Lecture Notes in Computer Science, 449, July 1990.
[Rit91] Mikael Rittri. Using types as search keys in func- tion libraries. Journal of Functional Programming, 1(1):71- 89, 1991.

Unification

[Rit93] Mikael Rittri. Retrieving library functions by unifying types modulo linear isomorphism. RAIRO Theoretical Informatics and Applications, 27(6):523-540, 1993.
[DJ90]
Equality [SE94]

With modules

[Mul; ZW93] ADC96; ADCD97

Serialization

To speed up database deserialization, we could use a format that allows random access in an mmap datastructure. Example of such formats:

Cap'n Proto (OCaml implementation: capnp)
Flatbuffer (No OCaml implementation)