Dot notation.

[higherorderco]

Dot notation.

[expede]

Just my two cents: dot syntax would conflict with module syntax readability, composition operator ((.)), and any potential future record syntax in the style of Elm. Not to say that these features will become available (I just discovered this project!), but using a dot in the way proposed limits other idioms more common in languages similar to Formality.

Something similar: OCaml, F#, and Elixir have a pipe operator behaves the same way, which may be a nice compromise. Elm and TypeScript also have pipes, but they do different things with order. Haskell has a library that provides them, too.

# Elixir
foo(a, b, c) == a |> foo(b, c)

This also chains applications nicely in diagrammatic order:

# Elixir

a
|> foo(b, c)
|> bar(d)
|> baz(e, f, g)

I would assume that this would be easy to implement as an infix function in Formality.

-- Formality
infixl 0 |>
let (X : Type) |> (F : X -> (Y: Type)) =>
  f(x) : Y

There's probably a bunch of syntax errors — sorry! (Just working from the README examples.) I don't see any fixity declarations, so I just used the Haskell/Idris one. So maybe this isn't possible, but infix operators would be useful, and more flexible than a special "dot-call" syntax / fluent interface.

[KiaraGrouwstra]

this feels OOP-like, running counter to the order normally used for currying?

[Kesanov]

• Formality does not have currying.
• It is a concept orthogonal to OOP, called infix operator.
• Even haskell has this: a `foo` b

[VictorTaelin]

Formality is fully curried, but I agree the syntax is misleading. (a : A, b : B) => c is just a syntax sugar for (a : A) => (b : B) => c. Same for forall and applications.

I like a.foo(b, c) as a syntax sugar for foo(a, b, c). But that alone won't make Formality a readable language. A lot else must be done for that. I have many ideas that I want to explore when we have Ethereum's upcoming browser. For now, let's keep it simple, even if it isn't the most aesthetically appealing language. We already have Agda, which is beautiful (and, probably, for a long time, using Agda will probably be the best way to write Formality).

[Kesanov]

1. dot syntax would conflict with module syntax

   No. See Java, Python, Elm ...

2. composition operator ((.)),

   No. You do not have to define composition as .. See Elm <<.

3. and any potential future record syntax in the style of Elm.

   No. See 1). record syntax is just dot notation for autogenerated row polymorphic functions.

4. I would assume that this would be easy to implement as an infix function in Formality.

   Formality does not have infix functions. Implementing custom infix functions is harder, then hard coding dot operator.

[VictorTaelin]

I'm moving away from a higher-level language with (arguably very limited) native datatypes to a lower-level language with a constellation of λ-encodings. User-friendlier syntaxes such as pattern-matching, datatypes and what is proposed here should and could be added on top of Formality as a separate pre-processing step. As such, this issue is now obsolete.

[VictorTaelin]

@Josef-Vonasek Just wanted you know that Formality-Lang (https://gitlab.com/moonad/formality-javascript) now allows you to address matched fields with the dot notation, which is actually kinda fake because it is just the variable name, but it is beautiful:

Nat.double :! {|*n : Nat} -> Nat
| succ = Nat.succ(Nat.succ(Nat.double(n.pred)))
| zero = Nat.zero