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 of steady typing

Preceding summary of key aspects:

• Inferred types are persisted to permanent storage
  This is against uncontrolled propagation of types when re-inferring them without taking into account the history of user action
  This is against gross misattribution of type errors far away from the relevant site.
• Type mismatches are made local explicit objects, here they are called fragments
• Fragments appear predictably at the last user edit
• Fragments can be shifted (shifting blame)
  This is against local misattribution of type errors. Putting the user into the drivers seat.
• Fragments shift predictably to the nearest,
  that is thanks to the persisted inferred types,
  is manual disambiguation needed in some cases?
• Verbosity: no chains of consequential errors far away from user actions and intent (not in the video but important)
• Verbosity: amount of progressive disclosure of types and values can be user adjusted as the situation affords.
• Live values flowing around type errors in other code branches remain visible.

---

Note: In all the following code-blocks:
The lines (or paragraphs) are results of successive user code edits.

Type assisted editing

🙁 Bad in C++ & Haskell: Types only available when the code is valid.

sum <| filer (1 … [🕳️]:Num) (keep※ x -> [🕳️]:Bool)
sum <| filer (1 … [🕳️]:Num) (keep※ x -> {x:Num}:Bool)

Step taken here:

• enter into the hole which is Num since keep※ is a function supposed to operate on List Num,
  this generates a type mismatch fragment

Liberties taken in syntax adaption:

• I've added <| which means a backet around everyting to the right
• I've added ※ to more conspiciously mark the unusual usage of the parameter name in the call

---

The type mismatch is localized with the fragment,
– so everything is still validly typed.
– so we still have 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 (C++, Haskell) 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 without enormous 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

Steps taken here:

• Changing the input value till the branch with the type mismatch is hit.
• Last step just makes hole pop up to visibility when the (here invisible) cursor arrives.

Liberties taken in syntax adaption:

• All made into one liners
• shown values are inserted in this ad-hoc form: "expession≔<value>" (may be a bad choice)
• I kept the "«" prefix as it seems to be a marker for type constructor in the demo video (odd choice)

Errors

Example:

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

Steps taken here:

• adding in the string "Hello" in the first branch
• adding in the integer 5 in the second branch,
  thereby causing a type mismatch,
  that mismatch appears at the site of the last edit, predictably so!
• insisting on this being correct shifting the type error over to the other branch

Liberties take in is syntax adaption:

• all made into one liners here
• removed the vertical bars
• [🕳️]:Bool … hole of type bool
• {} … here I used curly braces for the type mismatches (red outlined in the video), maybe not the best choice
• {value:Type} [🕳️]:Type … a type mismatch in the form of a "fragment"
• {value:Type}:Type … same thing the hole is just hidden away

---

There are type mismatch fragments.
One can insist on a type. This refragments the code.
In the 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 mismatches have a friendly user experience (UX).

Propagating API changes

🙁 Free propagation of type information with type inference can make things complicated.
🙂 Solution: Stop free type propagation from re-inferring types dead in it's tracks by persistently storing inferred type information.
That is: Types (inferred types) for all dependencies are (invisibly) stored.

>>> sumOfDigits 12345
sumOfDigits num = sum digits num
digits num = id (num==0): | «List empty. else: | (num % 10) :: digits (num // 10) 

>>> sumOfDigits 12345
sumOfDigits num = sum digits num
digits num base = id (num==0): | «List empty. else: | (num % 10) :: digits num※ (num // 10) base※ [ ]:b 

>>> sumOfDigits 12345 ⇝ ⚠️ Dependency type needs update
sumOfDigits num = sum digits⚠️ num
digits num base = id (num==0): | «List empty. else: | (num % base) :: digits num※ (num // base) base※ base

>>> sumOfDigits 12345 ⇝ ⚠️
sumOfDigits num = sum digits⚠️(OLD: Num -> List Num; NEW:{num※ Num, base※ Num} -> List Num) num
digits num base = id (num==0): | «List empty. else: | (num % base) :: digits num※ (num // base) base※ base

>>> sumOfDigits 12345 ⇝ NOTHING
sumOfDigits num = sum digits num※ [ ]:Num base※ [ ]:Num
digits num base = id (num==0): | «List empty. else: | (num % base) :: digits num※ (num // base) base※ base

>>> sumOfDigits 12345 ⇝ 15
sumOfDigits num = sum digits num※ num base※ 10
digits num base = id (num==0): | «List empty. else: | (num % base) :: digits num※ (num // base) base※ base

The steps taken above in sequence

• add the extra parameter "base"
• fill in the holes and show the type information
• show the dependency type mismatch details
• fill in the parameter template with holes fixing the type error but still leaving missing values
• fill in the fed through num parameter for num※ and 10 for base※ => works again

Some liberties taken in changing the syntax here:

• made it all one-liners (as mediawiki makes indentation editing hard and for these examples one liners are manageable)
• added a post-fix "※" for the in call parameter name usage
  all the following is the parameter till the next parameter name with a "※"

The sumOfDigits function uses previous type for type inference.
– Allowing everything to still be validly typed.
– Allowing to update dependencies one step at a time.

---

Heads up to some confusing aspects that I have noticed in the demo video. These compound.

• For "base※ base" which is direct parameter feed-through some obfuscating syntactic sugar is used taking the form "=> base"
• The first part of the type "{num※ Num, base※ Num} -> List Num" has a line-break added
  and one thus easily misreads it as "{num※ Num, -> List Num¶base※ Num}" which is incomprehensible nonsense, the absent ※ makes it worse.
• The positions of the arguments swap, that is enabled to be possible by the name addressing but for the demo it is confusing
• List concat "::" in the video is ":: |", I could not make sense of it so I removed the "|" here.

External links

Lamdu – Steady Typing – Yair Chuchem & Eyal Lotem – A novel UI for static types