[some_thoughts]

So I have very little experience with elixir, but I appreciate the effort to bring static typing. With that said, I find the use of parenthesis pretty hard to read. As in I need to spend more time than a quick glance to grok what's going on. Maybe it's because I'm not familiar with the ecosystem, but coming from a typescript, python, and go background mostly, I find this

negate :: ((integer() -> integer()) and (true -> false) and (false -> true) and (a -> a) when a: not(integer() or boolean()))

harder to reason about quickly than say this

negate :: (int -> int) & (true -> false) & (false -> true) & (a -> a) when a: ~(int | boolean)

Is there a reason that syntax was chosen? Is it just for showcasing purposes or is that basically just how the language works?

[josevalim]

For the paper, we have decided to go as precise as possible, since its goal is to discuss the type-system semantics and not its syntax, so parentheses are everywhere.

You will for sure be able to drop the outer parens in your case and you _may_ be able to drop them on the function types too (to be decided). Ending up with something like this:

    $ (integer -> integer) and (true -> false) and (false -> true) and (a -> a) when a: not(integer or boolean)
    def negate(arg)

We will also allow intersections to be broken across multiple declarations:

    $ integer -> integer
    $ true -> false
    $ false -> true
    $ a -> a when a: not(integer or boolean)
    def negate(arg)

[MartinMond]

In your example, how can the compiler (or a human) know that int is a concrete type as opposed to an unconstrained type variable?

Consider these two function signatures:

map :: ([a] -> [a])

map :: ([int] -> [int])

Furthermore the syntax that Elixir uses here let's you do something like

map :: (list(a) -> list(b))

list_to_other_data_structure :: (list(a) -> other_data_structure(a))

It all reminds me a bit of how Haskell does it https://medium.com/functional/haskell-basic-types-and-type-v...

I'm now curious to know if/how the above 'generics' would be expressed in TypeScript/Python/Go without a similar 'type constructor' syntax construct?

[laszlokorte]

A simple syntax would be something like

map :: forall a. ([a] -> [a])

or

map :: <a> ([a] -> [a])

[giraffe_lady]

At least in the current system I think the parens are optional if it doesn't have arguments so if you really need to leave them off when writing the type you probably can. But like someone said it's erlang convention going back decades.

Anyway coming from ocaml I don't aesthetically like this but coming from ocaml I have no grounds to talk shit about any language's aesthetic choices. The parens make sense to me when I think of them as type constructors, rather than concrete expressions of the type itself.

[masklinn]

It’s how types have been specified in erlang for 20+ years: https://www.erlang.org/doc/reference_manual/typespec.html

If you look at any erlang api doc, you’ll see predicate-like type specs. Conveniently, it naturally supports generics by just adding “parameters” to the predicates, so a dict would have type.

It works fine, and makes things less ambiguous, as erlang “types” can contain enumerations of values, in the original spec it’s clear that `integer()` is a type and `false` is a value, in your version not so much.