How to express the type of upcase?

[xuchunyang]

;; (test :: String -> String)
(defun test (s)
  "Upcase or downcase S."
  (if (string-prefix-p "#" s)
      (upcase s)
    (downcase s)))

Elsa reports the warning:

Function is expected to return String but returns Mixed.

C-h f upcase says:

The argument may be a character or string. The result has the same type.

How to express such type in Elsa?

[Fuco1]

It would be (String -> String) | (Int -> Int), I think the char type is not separate from integers.

I'm not sure how well the analysis in elsa will work though. But please report back, this is pretty interesting example.

[xuchunyang]

Now Elas reports:

Function is expected to return String but returns (String -> String) | (Int -> Int).

[Fuco1]

Oh, you wanted a signature for the test function. That would be String -> (String | Int). What I wrote was a type for upcase or downcase.

However, since you say that a string comes in it really has to be string coming out.

If we provide a type for upcase and downcase then the analysis should work better. But I'm not sure if resolution of unions of function types is implemented yet. A quick test suggests that it isn't.

[xuchunyang]

The warning in my previous comment is produced after I put the following in elsa-typed-builtin.el, the function test's signature is unchanged:

(put 'upcase 'elsa-type (elsa-make-type (String -> String) | (Int -> Int)))
(put 'downcase 'elsa-type (elsa-make-type (String -> String) | (Int -> Int)))

By the way, I expected the following emits warnings (e.g., the argument is not string or int) but I didn't:

(upcase 'test)
(downcase [1])

[Fuco1]

Yes, I tried the same thing you did and I looked at the code, the unions of functions are not analyzed, so that's not going to help. What you can write is (String | Int) -> (String | Int) but this is less specific because it allows e.g. string input and int output.

[Fuco1]

The function sum types (also known as function overloads) are now supported since 6f8d7509b24c9320f1e0e8462a20b42320cb68ce.

Note that the annotation syntax changed to a more lisp-like one

;; (test :: (function (string) string))
(defun test (s)
  "Upcase or downcase S."
  (if (string-prefix-p "#" s)
      (upcase s)
    (downcase s)))

this now type checks without problems. The actual type for downcase and upcase is (or (function (int) int) (function (string) string))