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.
🙂 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 paramerter template with holes fixing the type error but still leaving missing values
- fill in the fed through num paramater for num※ and 10 for base※ => works again
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.
Some liberties taken in changing the syntax here:
- made it all one-liners (as mediawiki makes identation editing hard and for these examples one liners are managable)
- added a postfix "※" for the in call parameter name usage
all the following ius the paraneter till the next parameter name with a "※"
Heads up to some confusing aspects that I have noticed in the demo video. These compound.
- For "base※ base" which is direct parameter feedthrough 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