How does Idris know where to insert Force and Delay?

user_11336776 0
Viewed 55

According to the Idris crash course:

The Idris type checker knows about the Lazy type, and inserts conversions where necessary between Lazy a and a, and vice versa.

For example, b1 && b2 is converted into b1 && Delay b2. What are the specific rules that Idris uses when deciding where to place these implicit conversions?

idris lazy-evaluation functional-programming
1 Answers

IIRC it's simply based on the unification of the provided type and the expected type. (&&) has type Bool -> Lazy Bool -> Bool. Unifying the second argument with y: Bool converts it to (delay y) value. On the other hand, if you'd pass x : Lazy Bool as the first argument, it converts to (force x). And this will be done with any values/function with Lazy a types.

user_57869500
Related