Conversation

So this conversation reminds me of a question about parameters with default arguments (e.g. Agda {x} parameters)... One can imagine a Python-like language where the writer of a function provides the defaults, with syntax something like "{x = DEFAULT : T} → U". twitter.com/pigworker/stat

This Tweet is unavailable.

Alan Jeffrey

@asajeffrey

Feb 23, 2020

Such a feature (plus a few others like invertable type constructors, and typeof) would deal with a lot of the cases that type inference is usually used for. For example "reverse: {A = List⁻¹(typeof(x)) : Set} → (x : List(A)) → List(A)".

Alan Jeffrey

@asajeffrey

Feb 23, 2020

(Variable scope here is odd, normally variable scope is L-R but here x is being mentioned in typeof(x) despite x being bound later, so there is some kind of recursion going on.)

Alan Jeffrey

@asajeffrey

Feb 23, 2020

So question... Is there prior art for this? Would it fly?

Brendan Zabarauskas

@brendanzab

Feb 23, 2020

Idris has default implicit arguments - not sure if it's what you are after though! docs.idris-lang.org/en/latest/tuto cc.

Hmm, I wonder how far they could be pushed as a replacement for type inference?

Replying to

and

Ohhh, I just saw `reverse: {A = List⁻¹(typeof(x)) : Set} → (x : List(A)) → List(A)` - which looks like it requires something like insanely dependent types. Yeah, Idris can't do this! github.com/UlfNorell/insa

9:10 PM · Feb 23, 2020Twitter Web App