Define Primer-the-language about primer HOT 19 CLOSED

How do we handle constructors?
The two options are

• Traditional non-bidirectional style: constructors are terms in-and-of themselves, and are synthesisable. Thus one has Cons ∈ ∀a. a -> List a -> List a, and Cons @Int 3 ∈ List Int -> List Int.
• Dogmatic bidirectional style: constructors must be fully applied, and are checkable (recall, bidirectional style says "constructions are checkable, eliminations are synthesisable"). Thus Cons is not well-typed on its own: in particular ∀a. a -> List a -> List a ∋ Cons is false. One instead has List Int ∋ Cons 2 Nil. To use constructors as functions, one must eta-expand thus: map (\n -> Succ n) ∈ List Nat -> List Nat. Notice that in this style constructors do not contain their parameters -- we have List Int ∋ Cons 2 Nil rather than Cons @Nat 2 (Nil @Nat). This works because we always know the exact type we are considering when looking at a constructor, and that tells us the parameters. We also can have different types having constructors with exactly the same name (in the core AST) and not worry about disambiguating them -- however this is a very minor concern for a structure editor since it is trivial to pun/disambiguate in the UI.

from primer.

Another definitional thing to hash out: can type constructors or value constructors be named the same thing as term definitions?

And, (https://github.com/hackworthltd/vonnegut/pull/844#discussion_r708269938) what do holes mean inside typedefs? data T = C (List ?). Should they be forbidden? It is easy to enforce this (indeed, our current frontend does), but may be awkward to change the generators used in testing to obey this.

from primer.

We should expose lettype to students, rather than having it only appear in eval mode. I think @brprice has indicated that this shouldn't be difficult, but we probably want to formalise it anyway.

from primer.

Do we want (and if so, in a 1.0, or sometime later) an analogue to Haskell's typeclasses, or maybe some other "get the compiler to write code for us" feature? It would be worth roughly answering this early as it will interact with other design decisions (we should avoid backing ourselves into a corner where it is hard to add this feature).

A useful (rather old) publication is Simon Peyton Jones Mark Jones Erik Meijer : Type classes: an exploration of the design space

from primer.

We have discussed several times that we eventually want to have richer patterns, in particular wildcards (necessary in practice to have pattern matching on primitives) and nested patterns.

(we don't expect this to make it in to Primer 1.0, and there's a lot more to say on the topic, but I need somewhere to link to whenever the future of patterns comes up)

from primer.

Edit I moved the contents of this comment to the OP.

from primer.

I don't know if the following would come under "typography" or "namespaces" or if it is a different suggestion.

Some languages will allow you to use the module system to distinguish local and global vars, e.g.

module Main where
foo :: Bool -> Nat
foo = ...

bar :: Char -> Nat
bar = λa . foo (a == 'x')

baz :: Bool -> Nat
baz = λfoo . Main.foo foo

where foo means "the most locally bound foo", but Main.foo means "the global foo"

from primer.

I don't know if the following would come under "typography" or "namespaces" or if it is a different suggestion.

I view this as a namespace solution.

Some languages will allow you to use the module system to distinguish local and global vars, e.g.

module Main where
foo :: Bool -> Nat
foo = ...

bar :: Char -> Nat
bar = λa . foo (a == 'x')

baz :: Bool -> Nat
baz = λfoo . Main.foo foo

where foo means "the most locally bound foo", but Main.foo means "the global foo"

Does Haskell? I've never tried to do this in the same module as where foo is defined.

from primer.

foo means "the most locally bound foo", but Main.foo means "the global foo"

Does Haskell? I've never tried to do this in the same module as where foo is defined.

Yes (at least, GHC 8.10.4)

from primer.

edit: I moved the contents of this comment to the OP.

from primer.

It might be time to put this in a Craft document, which would be easier to collaboratively edit.

from primer.

We should expose lettype to students, rather than having it only appear in eval mode. I think @brprice has indicated that this shouldn't be difficult, but we probably want to formalise it anyway.

Shower thought: exposing lettype in the language, and especially adding it to a modules-as-records implementation, means that unqualified constructor names are now potentially free variables in some scopes! Ignore this please, I'm not sure it made sense.

from primer.

We should expose lettype to students, rather than having it only appear in eval mode. I think @brprice has indicated that this shouldn't be difficult, but we probably want to formalise it anyway.

I've added this to the main list now.

from primer.

Do we want (and if so, in a 1.0, or sometime later) an analogue to Haskell's typeclasses, or maybe some other "get the compiler to write code for us" feature? It would be worth roughly answering this early as it will interact with other design decisions (we should avoid backing ourselves into a corner where it is hard to add this feature).

A useful (rather old) publication is Simon Peyton Jones Mark Jones Erik Meijer : Type classes: an exploration of the design space

I've added a note about this to the main list.

from primer.

Another definitional thing to hash out: can type constructors or value constructors be named the same thing as term definitions?

And, (hackworthltd/vonnegut#844 (comment)) what do holes mean inside typedefs? data T = C (List ?). Should they be forbidden? It is easy to enforce this (indeed, our current frontend does), but may be awkward to change the generators used in testing to obey this.

These are now captured in the main list.

from primer.

How do we handle constructors? The two options are

• Traditional non-bidirectional style: constructors are terms in-and-of themselves, and are synthesisable. Thus one has Cons ∈ ∀a. a -> List a -> List a, and Cons @Int 3 ∈ List Int -> List Int.
• Dogmatic bidirectional style: constructors must be fully applied, and are checkable (recall, bidirectional style says "constructions are checkable, eliminations are synthesisable"). Thus Cons is not well-typed on its own: in particular ∀a. a -> List a -> List a ∋ Cons is false. One instead has List Int ∋ Cons 2 Nil. To use constructors as functions, one must eta-expand thus: map (\n -> Succ n) ∈ List Nat -> List Nat. Notice that in this style constructors do not contain their parameters -- we have List Int ∋ Cons 2 Nil rather than Cons @Nat 2 (Nil @Nat). This works because we always know the exact type we are considering when looking at a constructor, and that tells us the parameters. We also can have different types having constructors with exactly the same name (in the core AST) and not worry about disambiguating them -- however this is a very minor concern for a structure editor since it is trivial to pun/disambiguate in the UI.

This is now addressed in the main list, and reflects our decision that they should be synthesizable.

from primer.

We have discussed several times that we eventually want to have richer patterns, in particular wildcards (necessary in practice to have pattern matching on for primitives) and nested patterns.

(we don't expect this to make it in to Primer 1.0, and there's a lot more to say on the topic, but I need somewhere to link to whenever the future of patterns comes up)

Added.

from primer.

We discussed this issue at length in our 2022-03-22 Primer definition meeting. I've updated the OP now to reflect all of our thinking as of this date.

I think it's now time to open tracking issues for each specific item in the OP, and to close this issue, as it has served its purpose.

from primer.

Each sub-issue described in the OP that has survived the "what should we include in Primer's language definition?" is now tracked by its own separate issue. Therefore, I'm now closing this issue.

from primer.