5 ms·

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 r

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?

MartinMond 3y ago
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-variables-dbb8efa86288 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 3y ago
  A simple syntax would be something like map :: forall a. ([a] -> [a]) or map :: <a> ([a] -> [a])
masklinn 3y ago
It’s how types have been specified in erlang for 20+ years: https://www.erlang.org/doc/reference_manual/typespec.html 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.
josevalim 3y ago
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)
giraffe_lady 3y ago
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.

MartinMond 3y ago

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-variables-dbb8efa86288 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 3y ago
A simple syntax would be something like map :: forall a. ([a] -> [a]) or map :: <a> ([a] -> [a])

masklinn 3y ago

It’s how types have been specified in erlang for 20+ years: https://www.erlang.org/doc/reference_manual/typespec.html 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.

josevalim 3y ago

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)

giraffe_lady 3y ago

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.