Conversation

Why on Earth not

3

9

Brendan Zabarauskas

You get annoying ambiguities with the dependent function syntax - ie. `(A : Set) -> A` - is this a non-dependent function from `A -> A` with the first `A` annotated, or is it a dependent function with a parameter named `A`?

2

1

Brendan Zabarauskas

Replying to

and

I'm most frustrated by this in my own language: github.com/pikelet-lang/p - arrrgh!

12:19 AM · Feb 26, 2019Twitter Web Client

Brendan Zabarauskas

Replying to

and

For now in github.com/brendanzab/rus I've decided to use a keyword to disambiguate it `Fun (A : Type) -> A` - still not super happy though. 😰