Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Church numeral sizing (finding computation limits) #69

Open
sfultong opened this issue Jun 27, 2021 · 1 comment
Open

Church numeral sizing (finding computation limits) #69

sfultong opened this issue Jun 27, 2021 · 1 comment

Comments

@sfultong
Copy link
Collaborator

All recursion in Telomare should be restricted to a limit of a certain number of recurrences.

The current plan is to use church numerals as fixed-point combinators to allow recurrence up to the magnitude of the church numeral. But for convenience, we don't want to make the user choose the magnitude of the church numeral. Telomare should do that itself automatically. That is what this issue is about.

A concrete example:

map = \f -> let layer = \recur l -> if l then (f (left l), recur (right l)) else 0
                base = \l -> 0
            in ? layer base

map succ [1,2,3]

The '?' here is a placeholder for the church numeral. Map will be compiled specifically for everywhere it is used. In this example, it is used with a list of 3 elements, so we want '?' to be replaced by the church numeral of (3 + 1 for the list terminator = 4).

Currently, we're attempting to implement this as a two stage process. The first stage is build a collection of expressions that can be tested to see if an arbitrarily-chosen church numeral is sufficient to make the expression evaluate correctly. The second stage is running all these expressions with a binary search to find the optimal church numeral, although this stage could probably be replaced by something faster and perhaps less precise.

Stage 1: how do we build an expression that can be tested to see if a church numeral is big enough?
The first thing to notice about the map example above, is that base should never actually be run. It's a placeholder to make the expression type check. Because we know that it never should be run, we can actually wrap it in another expression that aborts with a specific signal when it is executed. This way, we can simply run the test expressions and check to see if they evaluated to this abort signal, and if they did, we know that the church numeral we plugged in wasn't big enough.

Stage 2 should be pretty simple, and probably doesn't need elaboration.

@sfultong
Copy link
Collaborator Author

In the long term I would like to be able to write code that generates "infinite" sequences that are then truncated elsewhere (think take 5 listOfAllPrimeNumbers), but I will probably do a simpler approach that doesn't support this in the near term.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant