search

robrix / path

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

Multiplicities should be inferred #86

Open robrix opened 5 years ago

robrix commented 5 years ago

Omitting the multiplicities in a type should infer them and annotate the resulting type with the actual usages. E.g. const might be inferred to be:

const : { a : 0 Type } -> { b : 0 Type } -> 1 a -> 0 b -> a

… or something.