Record keyword/sigil ambiguity bikeshedding

[brendanzab]

I'd like to use bare braces for implicit arguments (see #8), so we'll need a keyword or sigil for dependent record syntax (see #2). Now, if I just used a single identifier, like record, for record types and record values, I would run into the following ambiguity:

Pikelet> :t record {}

Is this an empty record value, or the type of an empty record?

If we were going to have default fields then we would run into a similar issue:

Pikelet> :t record { x : I32 = 23 }

Is this a record value with a field annotated with a type I32 and a value 23, or is it a record type with a field of type I32 and a default value 23?

One way to resolve this would be to defer this choice to type checking, and require annotations in ambiguous circumstances. Bidirectional checking should make this trivial, but I'm not sure how nice it would be ergonomically.

Idris has a similar ambiguity around (), which can stand for the 'unit value' or the 'unit type'. It however defaults to the unit value in ambiguous circumstances, and coerces to a type or value when it has the necessary type information:

Idris> ()
() : ()
Idris> the () ()
() : ()
Idris> the Type ()
() : Type

Another option would be to have two different keywords, but then I have to decide on that:

• Record/record is one way, using a capital to signify the change in universe level
• Struct/struct - would convey more of a feeling of that fact we want a non-uniform memory representation
• sig/struct, like in ML?
• sig/record?
• signature/record - maybe a bit verbose?

[brendanzab]

Reposting some comments from Gitter:

@aatxe https://gitter.im/pikelet-lang/Lobby?at=5af303ad00dc488804a8994d

I'm inclined to say the second option [sig/struct] then since I think my preference is something like "no keywords > lowercase single word keywords > anything else"

@brendanzab https://gitter.im/pikelet-lang/Lobby?at=5afad494e0b50c2d05c3612f

One annoying thing about sig/struct is that they are really different in length. Looks kinda icky.
Also I find record to be a prettier word

@evincarofautumn https://gitter.im/pikelet-lang/Lobby?at=5afb2d7ef04ce53632dd1ad3

This is a hard one because it’s kind of an abstract distinction in English—what something is (thing/existence) versus what it is (type/attributes). Difference between “I am Jon” and “I am a human”.

record { .. } : record of { .. }
rec { .. } : rectype { .. }
data { .. } : datatype { .. }
{ .. } : {| .. |}
{| .. |} : { .. }
{ .. } : type { .. }

For the last one, type could put the parser in “type mode” to disambiguate. (In Kitten I was careful to make sure that it’s always clear whether you’re parsing a term or a type, so I can have overlapping grammars without ambiguity.)

[brendanzab]

One weird idea:

foo : {| x : Int, y : String |}
foo = (| x = 1, y = "hello" |)

[canndrew]

I don't really like the record syntax. It will make it extremely ugly to write nested records. Would it be better to use a different syntax for implicit args instead? Maybe you could use a sigil like

id: ?(a: Type) -> (x: a) -> a
id: '(a: Type) -> (x: a) -> a

(Sorry if this was already discussed on gitter. Also, this looks like a really cool project 👍 💯.)

[brendanzab]

Yeah, no worries!

It will make it extremely ugly to write nested records.

I agree too fwiw. A different sigil for implicit args could definitely be a solution. 🤔

[brendanzab]

(Sorry if this was already discussed on gitter. Also, this looks like a really cool project 👍 💯.)

Don't worry about repeating stuff from Gitter. I try to make sure stuff eventually ends up on Github in a less ephemeral form, so appreciate the chatting and discussions on here! I realise that it's sometimes easier for people to dip in and out of the issues at their leisure rather than keeping up to date with the chat. Also, I appreciate the compliments, it means a lot!