Steady typing - Revision history

Apm: /* Related */ added link to page Typed holes

2026-07-18T14:58:11Z

Related: added link to page Typed holes

← Older revision		Revision as of 16:58, 18 July 2026
Line 175:		Line 175:

	* [[Mechadense's wish programming language]]		* [[Mechadense's wish programming language]]
			* [[Typed holes]]

	= External links =		= External links =

	[https://www.youtube.com/watch?v=viF1bVTOO6k Lamdu – Steady Typing – Yair Chuchem & Eyal Lotem – A novel UI for static types]		[https://www.youtube.com/watch?v=viF1bVTOO6k Lamdu – Steady Typing – Yair Chuchem & Eyal Lotem – A novel UI for static types]

Apm: /* Errors & shifting of type mismatch blame */

2026-06-23T18:48:51Z

Errors & shifting of type mismatch blame

← Older revision		Revision as of 20:48, 23 June 2026
Line 87:		Line 87:
	if [🕳️]:Bool then [🕳️]:a else [🕳️]:a		if [🕳️]:Bool then [🕳️]:a else [🕳️]:a
	if [🕳️]:Bool then "Hello":String else [🕳️]:String		if [🕳️]:Bool then "Hello":String else [🕳️]:String
	if [🕳️]:Bool then "Hello":~~tring~~ else {5:Num} [🕳️]:String		if [🕳️]:Bool then "Hello":String else {5:Num} [🕳️]:String
	if [🕳️]:Bool then {"Hello":String}:Num else 5:Num		if [🕳️]:Bool then {"Hello":String}:Num else 5:Num
	</pre>		</pre>

Apm: /* Errors & shifting of type mismatch blame */

2026-06-23T18:48:41Z

Errors & shifting of type mismatch blame

← Older revision		Revision as of 20:48, 23 June 2026
Line 86:		Line 86:
	<pre>		<pre>
	if [🕳️]:Bool then [🕳️]:a else [🕳️]:a		if [🕳️]:Bool then [🕳️]:a else [🕳️]:a
	if [🕳️]:Bool then "Hello":a else [🕳️]:String		if [🕳️]:Bool then "Hello":String else [🕳️]:String
	if [🕳️]:Bool then "Hello":a else {5:Num} [🕳️]:String		if [🕳️]:Bool then "Hello":tring else {5:Num} [🕳️]:String
	if [🕳️]:Bool then {"Hello":String}:Num else 5:Num		if [🕳️]:Bool then {"Hello":String}:Num else 5:Num
	</pre>		</pre>

Apm: /* Errors */ extended on the title

2026-06-23T08:38:37Z

Errors: extended on the title

← Older revision		Revision as of 10:38, 23 June 2026
Line 81:		Line 81:
	* I kept the "«" prefix as it seems to be a marker for type constructor in the demo video (odd choice)		* I kept the "«" prefix as it seems to be a marker for type constructor in the demo video (odd choice)

	== Errors ==		== Errors & shifting of type mismatch blame ==

	'''Example:'''		'''Example:'''

Apm: /* Errors */ fixed mistake in types of example

2026-06-23T08:35:25Z

Errors: fixed mistake in types of example

← Older revision		Revision as of 10:35, 23 June 2026
Line 88:		Line 88:
	if [🕳️]:Bool then "Hello":a else [🕳️]:String		if [🕳️]:Bool then "Hello":a else [🕳️]:String
	if [🕳️]:Bool then "Hello":a else {5:Num} [🕳️]:String		if [🕳️]:Bool then "Hello":a else {5:Num} [🕳️]:String
	if [🕳️]:Bool then {"Hello":a}:Num else 5:Num		if [🕳️]:Bool then {"Hello":String}:Num else 5:Num
	</pre>		</pre>

Apm: /* Aspects of steady typing */

2026-06-20T21:41:07Z

Aspects of steady typing

← Older revision		Revision as of 23:41, 20 June 2026
Line 21:		Line 21:
	'''Two major topics here:'''		'''Two major topics here:'''
	* A large part here is about preventing type error misattribution meta errors (that can make programming thoroughly unfun).		* A large part here is about preventing type error misattribution meta errors (that can make programming thoroughly unfun).
	* An other part here is about fully preserving liveness in visibility of both ~~types~~ types and values without any loss.		* An other part here is about fully preserving liveness in visibility of both types and values without any loss of cases.

	----		----

Apm at 21:40, 20 June 2026

2026-06-20T21:40:13Z

← Older revision		Revision as of 23:40, 20 June 2026
Line 4:		Line 4:
	Some twists on handling type inference and type mismatches. <br>		Some twists on handling type inference and type mismatches. <br>
	For holes [🕳️]:Type the type annotations are always shown. <br>		For holes [🕳️]:Type the type annotations are always shown. <br>
			<small>As there the user will want to know what to connect in detail.</small> <br>

	= Aspects of steady typing =		= Aspects of steady typing =

Apm: /* Aspects of steady typing */ Added major topics section and back-link to page linking here

2026-06-20T21:38:47Z

Aspects of steady typing: Added major topics section and back-link to page linking here

← Older revision		Revision as of 23:38, 20 June 2026
Line 18:		Line 18:

	----		----
			'''Two major topics here:'''
			* A large part here is about preventing type error misattribution meta errors (that can make programming thoroughly unfun).
			* An other part here is about fully preserving liveness in visibility of both types types and values without any loss.

			----
	Note: In all the following code-blocks: <br>		Note: In all the following code-blocks: <br>
	The lines (or paragraphs) are results of successive user code edits.		The lines (or paragraphs) are results of successive user code edits.
Line 166:		Line 170:
	* The positions of the arguments swap, that is enabled to be possible by the name addressing but for the demo it is confusing		* 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.		* List concat "::" in the video is ":: \|", I could not make sense of it so I removed the "\|" here.

			== Related ==

			* [[Mechadense's wish programming language]]

	= External links =		= External links =

	[https://www.youtube.com/watch?v=viF1bVTOO6k Lamdu – Steady Typing – Yair Chuchem & Eyal Lotem – A novel UI for static types]		[https://www.youtube.com/watch?v=viF1bVTOO6k Lamdu – Steady Typing – Yair Chuchem & Eyal Lotem – A novel UI for static types]

Apm: /* Aspects of steady typing */

2026-06-20T21:29:01Z

Aspects of steady typing

← Older revision		Revision as of 23:29, 20 June 2026
Line 8:		Line 8:

	'''Preceding summary of key aspects:'''		'''Preceding summary of key aspects:'''
	* Inferred types are persisted to permanent storage <br>This is against uncontrolled propagation of types when re-inferring them without taking into account the history of user action <bt>This is against gross misattribution of type errors far away from the relevant site.		* Inferred types are persisted to permanent storage <br>This is against uncontrolled propagation of types when re-inferring them without taking into account the history of user action <br>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		* Type mismatches are made local explicit objects, here they are called fragments
	* Fragments appear predictably at the last user edit		* Fragments appear predictably at the last user edit

Apm: /* Aspects of steady typing */ improvements on the discussion of type error misattribution meta errors

2026-06-20T21:28:46Z

Aspects of steady typing: improvements on the discussion of type error misattribution meta errors

← Older revision		Revision as of 23:28, 20 June 2026
Line 8:		Line 8:

	'''Preceding summary of key aspects:'''		'''Preceding summary of key aspects:'''
	* Inferred types are persisted to permanent storage <br>(against uncontrolled propagation of types when re-inferring them without taking into account the history of user action)		* Inferred types are persisted to permanent storage <br>This is against uncontrolled propagation of types when re-inferring them without taking into account the history of user action <bt>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		* Type mismatches are made local explicit objects, here they are called fragments
	* Fragments appear predictably at the last user edit		* Fragments appear predictably at the last user edit
	* Fragments can be shifted (shifting blame – against misattribution of ~~types)~~		* Fragments can be shifted (shifting blame) <br>This is against local misattribution of type errors. Putting the user into the drivers seat.
	* Fragments shift predictably to the nearest, <br>that is thanks to the persisted inferred types, <br>is manual disambiguation needed in some cases?		* Fragments shift predictably to the nearest, <br>that is thanks to the persisted inferred types, <br>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: no chains of consequential errors far away from user actions and intent (not in the video but important)