search

robrix / path

A lambda calculus to explore type-directed program synthesis.
BSD 3-Clause "New" or "Revised" License
83 stars 2 forks source link

Explicitize implicits #101

Closed robrix closed 5 years ago

robrix commented 5 years ago

This PR attempts to handle implicits in a more principled manner. We want to be able to ensure that:

fix : { a : Type } -> { b : Type } -> ((a -> b) -> a -> b) -> a -> b
fix = \ {a} {b} f . f (fix {a} {b} f)
≡
fix : { a : ? } -> { b : ? } -> ((a -> b) -> a -> b) -> a -> b
fix = \ {a} {b} f . f (fix {?} {?} f)
≡
fix : ((a -> b) -> a -> b) -> a -> b
fix = \ f . f (fix f)