Steady typing
Static typing and its benefits as base.
Some twists on handling type inference and type mismatches.
For holes [🕳️]:Type the type annotations are always shown.
Aspects
Type assisted editing
🙁 Bad in C++ & Haskell: Types only available when the code is valid.
Codeblocks: Each line after an user edit step.
sum <| filer (1 … [🕳️]:Num) (keep x -> [🕳️]:Bool)
sum <| filer (1 … [🕳️]:Num) (keep x -> {x:Num}[]:Bool)
The type mismatch is localized with the fragment,
– so everything is still validly typed.
– so we still the expected types for holes.
🙂 Types are steadily available even if the program is incomplete and has type mismatches.
I.e. type assisted editing is always available.
Type information and completions are available at all times.
Verbosity
🙁 Static type systems infamous for verbosity of type error messages.
🙂 All types can be shown at once (quite verbose) but they are hidden as default.
The reader controls the verbosity of type information.
Mismatches shown i right in the code witout eneromizs chains of consequential errors.
And without lack of control of blame. See section on errors.
Run code despite of type errors
🙂 Yes we can! Live coding with values being showable. Always!
favorites x = if (x==0) "R" elif (x==1) "W" else {«Maybe just:"S" : Maybe Text}:Text
favorites x≔<0> = (if (x==0)≔<true> "R" elif (x==1)≔<false> "W" else {«Maybe just:"S" : Maybe Text}[]:Text) ≔ <R>
favorites x≔<1> = (if (x==0)≔<false> "R" elif (x==1)≔<true> "W" else {«Maybe just:"S" : Maybe Text}[]:Text) ≔ <W>
favorites x≔<2> = (if (x==0)≔<false> "R" elif (x==1)≔<false> "W" else {«Maybe just:"S" : Maybe Text}[]:Text) ≔ NOTHING
favorites x≔<2> = (if (x==0)≔<false> "R" elif (x==1)≔<false> "W" else {«Maybe just:"S" : Maybe Text}[🕳️]:Text) ≔ NOTHING
Last line is makes hole pop up when the (here invisible) cursor arrives.
Errors
if [🕳️]:Bool then [🕳️]:a else [🕳️]:a
if [🕳️]:Bool then "Hello":a else [🕳️]:String
if [🕳️]:Bool then "Hello":a else {5:Num} [🕳️]:String
if [🕳️]:Bool then {"Hello":a}:Num else 5:Num
- [🕳️]:Bool … hole of type bool
- {5:Num} … a type mismatch in the form of a "fragment"
There are type mismatch fragments.
One can insist on a type. This refragments the code.
In example it shifts the fragment to the other branch.
Type errors are predictably assigned to the newest code edits.
The user is empowered to reassign the blame to (actually) conflicting code.
This fixes the problem of
propagation and misattribution of type errors
in static typing with type inference.
Type mismathces have a friendly user experience (UX).
Propagating API changes
🙁 Free propagation of type information with type inference can make thinks complicated.
🙂 (wiki-TODO: add another exmple fron the video)
External links
Lamdu – Steady Typing – Yair Chuchem & Eyal Lotem – A novel UI for static types