[erlang-questions] Orelse and andalso as short-hand for case

[Jesper Louis Andersen]

On Mon, Jul 23, 2018 at 3:32 PM Dmitry Belyaev <be.dmitry@REDACTED> wrote:

> How does it mess with types? The andalso and orelse operators should only
> care about the type of the first operand and it always is boolean.
>
>
​Assume a GADT or dependently typed language. Then we have something like
(forgive me the rust on the Agdaish notation used here):

data Ty where
  Bool : Ty
  Int : Ty

data Expr (t : Ty) : Set where
  andAlso : Expr Bool -> Expr Bool -> Expr Bool
  orElse : Expr Bool -> Expr Bool -> Expr Bool
  ...

​and this is the normal canonical definition most statically typed
languages use. You propose

data Expr (t : Ty) : Set where
  andAlso : Expr Bool -> Expr t -> Expr ?
  orElse : Expr Bool -> Expr t -> Expr ?
  ...

but the complication is that you have to be able to tell the system what
the '?' should be. It is some union type over either Bool or t for any type
t, but this easily complicates the type rules of the language. This is why
I say it is a "mess". You might come up with a solution, but that solution
will usually lead to an acceptance of a larger body of programs in which
some of the programs will be weaker from a type perspective. Or it will
lead to programs which has to do more runtime checking which are slower
programs.

Finally, in a dynamically typed language like Erlang, you indeed can give
it a somewhat meaningful result by your proposal. But my view, as it often
does, comes from 15 years of statically typed programming in Standard ML,
OCaml and Haskell.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20180723/32e15057/attachment.htm>