wende / elchemy

Write Elixir code using statically-typed Elm-like syntax (compatible with Elm tooling)
https://wende.github.io/elchemy/
MIT License
1.15k stars 28 forks source link

Find a way to express Elixir's "Either" type with guards #335

Closed wende closed 6 years ago

wende commented 6 years ago

In many Elixir libraries the types of arguments/fields in structs are expressed as an alternative of types in an non-idiomatic to typed languages way. For instance the Plug.Conn of Elixir has a field in Conn.t()

          resp_body: body | nil,

Where body is an iodata (String). That's clearly a distinction that can be tested against without being expressed in a form of Elchemy types (Tuple with an atom first). Elixir/Erlang uses guards for that in cases and functions.

An also good simple example of that would be a Maybe type which right now is solved as a half measure with a special case of Just a being {a} and Nothing being nil.

The system to solve that could be done using a special syntax for defining type guards.

The choice for making a Maybe this way was because of how pattern matching works. If we assumed Just a is a and Nothing is nil we'd get to a problems when trying to pattern match upon that:

case a of 
  Nothing -> 0
  Just a -> a

Would work by being translated to

case a do
  nil -> 0
  a -> a
end

However if the branches were put in an reversed order it would change the logic

case a do
  a -> a      # <-- nil would also get caught by this
  nil -> nil  # <-- This would never happen

To do that in an more elegant and more idiomatic way there could be a system to add guards when pattern matching on a type. Assuming a pattern match exists only in case _ of branches we could add special guards to make sure the value is what we're really trying to get. For instance with Maybe:

case a do
  a when !is_nil(a) -> a
  nil -> 0
end

Could be defined as (up to debate)

type Guard 
  = Not Guard
  | IsNil
  | And Guard Guard
  | Or Guard Guard
  | None

maybeGuard : Maybe x -> Guard
maybeGuard m =
  case m of 
    Nothing -> IsNil
    Just -> Not IsNil
wende commented 6 years ago

It appears that a problem occurs when trying to combine nested guarded types.

For instance having Just Nothing (of type Maybe (Maybe a)) would cause a problem of being Nothing and not being a just.

case nil do // Just Nothing
  a when is_nil(a) -> "This shouldn't match but it would
  a when not is_nil(a) -> "This won't match but should"
wende commented 6 years ago

After giving it a longer thought it appears that a nested guarded types create too much confusion. This idea might not be worth implementing after all and the recommended way to express types like that should be an adapter function (conversion to safer types in Elixir)