search

lorepozo / list-routines

Interactive dataset for program learning.
https://lucasem.github.io/list-routines/
MIT License
2 stars 0 forks source link

higher-order functions (map, filter, and fold) #3

Open joshrule opened 4 years ago

joshrule commented 4 years ago

The dependent type system that's currently in place works well for functions which take in lists of numbers or integers and output either lists, integers, or Booleans.

Have you thought about what would be required to add higher-order functions like map, filter, and fold, so that instead of baking in the iterating function (e.g. subroutines like add-k), we could also freely define those according to some DSL?

lorepozo commented 4 years ago

This would be really cool! I think it’s quite challenging — the work would include gutting the type system and integrating a constraint solver. Might even inspire a deeper re-architecture to use different programming languages — e.g. I think Idris or Lean would be more suited to something like this.

joshrule commented 4 years ago

Hmmm.... switching languages was my first thought, too. I was thinking something along the lines of prolog because of its strength in expressing and resolving disparate constraints, but a fully-dependently-typed language could be a good fit, too.