antitypical / Manifold

An implementation of a dependently-typed intermediate language used by Tesseract.
MIT License
30 stars 0 forks source link

Implicit arguments #155

Closed robrix closed 8 years ago

robrix commented 8 years ago

This is the definition of List.pure added in #154:

let pure = Declaration("List.pure",
    type: .Type => { A in A --> List.ref[A] },
    value: () => { A, a in cons[A, a, `nil`[A]] })

Syntax notwithstanding, this is much like in a “real” language. However, since there are no implicit arguments, we always have to apply the type parameters explicitly in the values of functions. This is (apparently) unnecessary! We should be able to reduce that down to:

let pure = Declaration("List.pure",
    type: () => { A in A --> List.ref[A] },
    value: () => { a in cons[a, `nil`] })

Apparently, implicit arguments will allow this. I just have no idea how they work.

robrix commented 8 years ago

Turns out I was conflating implicit arguments and type erasure. Filed #160 about erasure.

robrix commented 8 years ago

This was not closed by #161.

robrix commented 8 years ago

Looks like it requires unification.