Clearly report type errors on API boundary

[JaroslavTulach]

Currently Enso is using "duck typing" - e.g. one can invoke a function with any argument and if such argument has the right methods, fields, etc. as expected, the execution goes on. Such a behavior is causing issues in the IDE - when a wrong node is connected as an argument (a Text instead of Number for example), the execution isn't rejected immediately, but proceeds until the "duck typing" fails. However that is often late, deeply in the standard libraries internals and produces hard to understand errors. It'd be way better if the typing error was caught right on the API boundary.

type Num
    All a
    Value (x : Num)

Let's use the ascribed types for real type checks. With the above type definition, the following would execute OK: Num.All "ok", but invoking Num.Value "error" would rise a Type_Error. Similarly with a

check (n : Num) = n

Invoking check "error" shall yield an error while check (Num.All "ok") shall be fine. There is a proof of concept branch demonstrating it can all work.

[radeusgd]

How do we plan to check conditions like

foo (v : Vector Integer) = v.take 5

...

foo [1,2,3]
foo [1,2,"X"]
foo []

[radeusgd]

I guess one way to do it would be to just ignore the 'type argument' and check is_a Vector as this is what we can do - I'm however afraid the halfway typecheck may give the users a bit of false sense of security - but if it's the best we can do quickly I guess it's good, we just need to make sure users know about our 'erasure'.

Probably in library code we'd need to then ensure that we verify the type once read from the vector, like:

foo (vec : Vector Integer) =
    x : Integer = vec.first
    y : Integer = vec.second
    x + y

Still, it is a bit harder now to track the error, because the true error happens when calling foo with a wrong vector, but it may be caught much later (in the example above its just a line below, but in practice it may be much further apart).

However, again - I think this solution will still improve most use cases so greatly that it is of course worth doing even if it will not (yet) be perfect in the more complex errors.

[JaroslavTulach]

I think this solution will still improve most use cases so greatly that it is of course worth doing even if it will not (yet) be perfect in the more complex errors.

Implementing the "erasure" style is a matter of a week. Then the Enso type system can be on par with Java 1.4 (before the introduction of generics).

Implementing Vector Integer (or rather MyType Integer) is a more complex change. Making foo append(x: List a) (y : a) : List is even slightly more work.

[JaroslavTulach]

However recording type at the creation may give us "incomplete type":

type Either a b
    Left l : a
    Right r : b

probably foo (e : Either Text Integer) and boo (e : Either Boolean Integer) could both be invoked with Either.Right 5!

Thinking about it more, I think this leads to Julia-like type system:

• Only values ... have types
• Type parameters may be omitted when they do not need to be referenced or restricted
• attach type annotations to expressions and variables... as an assertion
• Point itself is also a valid type object, containing all instances Point{Float64}, Point{AbstractString}, etc. as subtypes
• Concrete Point types with different values of T are never subtypes of each other
• Point{Float64} is not a subtype of Point{Real}

[enso-bot]

Jaroslav Tulach reports a new STANDUP for yesterday (2023-05-22):

Progress: - Investigating ascribed types #6682

• PR: Runtime check of ascribed types #6790
• playing with support for Union types & from conversion problems
• Import & exports meeting to be on Wednesday: https://docs.google.com/document/d/11eorzTM4F3kYPGo6m5mooiUrmaUg_quEWbbr4rJpSbE
• bookclub: https://discord.com/channels/401396655599124480/1110164041474777128/1110240500377718884
• meetings, demos, triaging It should be finished by 2023-05-29.

Next Day: Runtime check of argument types

Google Docs

Notes - Imports/Exports discussion

| Tuesday May 24, 2023 ⋅ 3:15pm – 4pm Central European Time - Warsaw Join with Google Meet https://meet.google.com/ybj-spjf-nyk?hs=224 Attendees: Overview A discussion has recently been held in our discord channel touching topic of imports and exports in Enso. Here is a summary of what ...

Discord

Discord - A New Way to Chat with Friends & Communities

Discord is the easiest way to communicate over voice, video, and text. Chat, hang out, and stay close with your friends and communities.

[enso-bot]

Jaroslav Tulach reports a new STANDUP for yesterday (2023-05-23):

Progress: - Map.equals bugfix: #6803
- hasHashEntries implies being a Map: b5125a3
- speeding up MetaIsATest and making it polyglot: e2c7ed5
- emails, reviews, planning, standups, discussion, triaging
- code/data bug: #6809 It should be finished by 2023-05-29.

Next Day: Bugfixing & meeting about imports

[enso-bot]

Jaroslav Tulach reports a new STANDUP for yesterday (2023-05-28):

Progress: - "Fixing" some wrong constructor signatures: #6790 (comment) It should be finished by 2023-05-29.

Next Day: Bookclubs, bugfixing, ascribed types

[enso-bot]

Jaroslav Tulach reports a new STANDUP for yesterday (2023-05-29):

Progress: - store location of atom constructors: fe0edb0

• escribed types status: Runtime check of ascribed types #6790 (comment)
• review: https://github.com/enso-org/enso/pull/6849/files#r1207081296
• triaging: Text.find_all can loop endlessly #6856
• understanding imports/exports
• standup, talking to Dmitry, Sylwia, Radek
• Interfaces/Type classes in Enso: develop...JaroslavTulach:enso:wip/jtulach/interfaces
• Demo meeting; discussions It should be finished by 2023-05-29.

Next Day: Interfaces & ascribed types

GitHub

Append warnings extracted before tail call execution by hubertp · Pull Request #6849 · enso-org/enso

Pull Request Description Throwing TailCallException meant that exceptions that were extracted from the expression before the call was made could not be appended. This change catches the TailCallExc...

[enso-bot]

Jaroslav Tulach reports a new 🔴 DELAY for yesterday (2023-05-29):

Summary: There is 7 days delay in implementation of the Clearly report type errors on API boundary (#6682) task.
It will cause 7 days delay for the delivery of this weekly plan.

PR is ready for QA, but not integratable yet

Delay Cause: Runtime checks in Standard.Table constructors are detecting many violoations and causing failures of appropriate tests. We need to decide what to do with it and it's going to take some time.

Possible solutions: Wojciech suggests to design an annotation and only type check then. We can disable checks on constructors for now. We can add | Any to all constructors that report violation and fix incrementally then.

[enso-bot]

Jaroslav Tulach reports a new STANDUP for yesterday (2023-05-30):

Progress: - Runtime check of ascribed types is in: #6790

• Bugfixing runtime checks: Search for IR.Function deeper in the IR tree to find instance methods #6902
• bookclub: https://discord.com/channels/401396655599124480/1113051687838560347/1113082456799723550
• import/export meeting: https://docs.google.com/document/d/11eorzTM4F3kYPGo6m5mooiUrmaUg_quEWbbr4rJpSbE#heading=h.ilkxfw5rsv3g
• (demo) meetings It should be finished by 2023-06-05.

Next Day: Imports & Interfaces & ascribed types

Discord

Discord - A New Way to Chat with Friends & Communities

Discord is the easiest way to communicate over voice, video, and text. Chat, hang out, and stay close with your friends and communities.

Google Docs

Notes - Imports/Exports discussion

| 3rd meeting: June 6, 2023 3:15pm – 4pm, Join with Google Meet 2nd meeting: May 30, 2023 ⋅ 3:15pm – 4pm, Join with Google Meet 1st meeting: May 24, 2023 ⋅ 3:15pm – 4pm, Join with Google Meet Central European Time - Warsaw Motto Once upon a time there was a bug report: #6553 … and then a d...