CODEWITHSUNDEEP
functional-programminglazy-evaluationidris
Owen Bechtel
Owen Bechtel

Reputation: 148

How does Idris know where to insert Force and Delay?

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?

Upvotes: 4

Views: 95

Answers (1)

xash
xash

Reputation: 3722

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.

Upvotes: 3

Related Questions