Default/implicit record fields

[treeowl]

Arguments to a data constructor can be implicit, and can therefore be given default values or tactics. Class methods can offer default implementations. Records seem to offer neither.

[edwinb]

Feature requests such as this are significantly more likely to be implemented with some suggested syntax and a suggested way of elaborating them - I'm extremely unlikely to implement it otherwise. Here we'd need to think about the record declaration, and record construction with default.

[treeowl]

record Foo where
  constructor MkFoo
  implicit bar : Baz
  implicit baz : Quux
  baz = Refl
  implicit auto baz2 : Quux

I'd expect that to give me what I'd get out of

data Foo where
  MkFoo : {bar : Baz} -> {default Refl baz : Quux} -> {auto baz2 : Quux} -> Foo

[edwinb]

I'm not sure I like that elaboration - there seems to be something of a disconnect between the 'implicit' and the default expression despite the fact they are linked. What if bar is an explicit argument? Should it also work?

It feels a bit like adding a feature for the sake of it to me. This elaboration doesn't have any obvious correspondence to what happens with data or classes, it's just one more thing to learn.

On 18/05/2015 17:51, David Feuer wrote:

record Foo where constructor MkFoo implicit bar : Baz implicit baz : Quux baz = Refl implicit auto baz2 : Quux

I'd expect that to give me what I'd get out of

data Foo where MkFoo : {bar : Baz} -> {default Refl baz : Quux} -> {auto baz2 : Quux} -> Foo

— Reply to this email directly or view it on GitHub https://github.com/idris-lang/Idris-dev/issues/2267#issuecomment-103127072.

[treeowl]

Yes, it should also work, explaining what to do with a _ argument (which could presumably be extended elsewhere). There's no obvious-to-me reason that only implicits should have default resolution mechanisms.

The syntax for defaults should probably be changed a bit to be visually distinct from that of class defaults, which seem to act a bit differently. Unless, that is, the class defaults are changed to act the same.

Reasoning: there's a lot of overlap between class, record, and data functionality resulting in large part from the decision not to try to enforce some sort of class coherence. To the extent that these things are "about the same", I think they should probably offer the same features to the extent possible.

[ahmadsalim]

We can just be inspired by Agda's syntax.

record Foo where
  constructor MkFoo
  {bar} : Baz
  {default Refl baz} : Quux
  {auto baz2} : Quux

[david-christiansen]

This is a reasonable way to do it.

What's up with the bizarre highlighting?