Implicit types and optional parameters

Stream: new members

[Sébastien Boisgérault]

Hi everyone :wave:

I have just been surprised by an interaction between default (optional) parameters and type genericity.

The functions f and g

def f {α : Type} (a : α) : List α := [a]
def g (a := "") : List String := [a]

work without any problem but the hybrid function h

def h {α : Type} (a : α := "") : List α := [a]

does not typecheck. The error is

Application type mismatch: In the application
  optParam α ""
the argument
  ""
has type
  String : Type
but is expected to have type
  α : Type

Could anyone provide some context (and maybe a workaround?) for this situation?

Cheers!

Sébastien

[Yaël Dillies]

Hey :wave: What do you intend to do with this function h?

[Kenny Lau]

you want by exact to delay elaboration

[Aaron Liu]

def h {α : Type} (a : α := by exact "") : List α := [a]

-- h "" : List String
#check (h)

[Sébastien Boisgérault]

Yaël Dillies said:

Hey :wave: What do you intend to do with this function h?

In the real use case, h is oneOrMore:

partial def oneOrMore {α : Type} {β₁ β₂ β₃ : Type} (p : Parser α)
  (parsePrefix : Parser β₁ := parseNothing)
  (parsePostFix : Parser β₂ := parseNothing)
  (parseSeparator : Parser β₃ := parseNothing) : Parser (List α):= sorry

The default argument parseNothing is of type Parser Unit but I'd rather not force it for all parsers (for the prefix, separator and postfix I would just ignore the parsed value).

Does it help?

[Aaron Liu]

If you are ignoring the parsed value you should probably take a Parser Unit anyways to signal that

[Aaron Liu]

the value can be discarded at the call site with docs#Functor.discard

[Aaron Liu]

this is how do notation works

[Sébastien Boisgérault]

Aaron Liu said:

def h {α : Type} (a : α := by exact "") : List α := [a]

Thanks! That works for the toy example and for the real one AFAICT. A bit mysterious for me ATM but appreciated nonetheless! :pray:

[Sébastien Boisgérault]

Aaron Liu said:

the value can be discarded at the call site with docs#Functor.discard

I was in the process of implementing a drop function ... :grinning_face_with_smiling_eyes: