Jacob (Jul 18 2023 at 17:36): Jacob (Jul 18 2023 at 17:36):Just started looking at Roc this week and I love the effort! I'm super interested in decisions for language design and trying to learn about what goes into it, not particularly suggesting anything to be changed.
Any reason in particular that records need comma's to separate fields? In Lean you can do the following, but I am not knowledgeable enough to know if it's for a technical reason or something else. Thank you!
structure MyRecord :=
field₁ : Nat
field₂ : Prop
field₃ : α → β → γ
this looks a lot like what agda does. It's syntactically similar to what they do for sum types
Anton (Jul 18 2023 at 17:50):I do like the vertical style in isolation, but you do want to create records inline and then you would have two "styles" for working with records instead of one.
Jacob (Jul 18 2023 at 17:54):I haven't used Agda in a long time, so I had to double check. But records do pretty much the same thing for the fields.
Jacob (Jul 18 2023 at 17:56):Yeah, u do restrict that record definitions can't be inline (if u don't want separate syntax). Personally I like enforcing that (only for definitions).
Last updated: Jun 16 2026 at 16:19 UTC