Gradual Types

Dynamic type systems are known for ease of rapid development, but do not scale well with increasingly complex programs or libraries.

Gradual type systems provide a combination of a quick development pace and the ability to incrementally add rigor piece by piece.

This article discusses language features in Kronos, version 0.14, to enable gradual typing reminiscent of C++ concepts.

Power and Astonishment

A piece of wisdom from software engineering: the power of a feature should be adequate for its purpose, but not excessive.

In language design this relates to the implicit and explicit. When the compiler does things for you, the language becomes more powerful. However, when it does unexpected things for you, the results can be astonishingly wrong. I don't know about you, but astonishment is one of my least favourite emotions while running computer programs.

Hence, when a language feature does a lot of work under the hood, it is best to make it explicit. The programmer should at least have to give that imperceptible nod that says "Yes, I know what I'm doing."

Maturing the Language

The initial vision for Kronos was far more simplistic than what the language has evolved into. The polymorphic mechanism was there primarily to help unit generators support different channel counts and sample formats. I did not realize its applicability to things like closures or the emergent Turing completeness.

That's why the language defaults started as too powerful. Each polymorphic reification would involve a depth-first search of any legal combination of forms, with illegal callees causing callers to be illegal.

A type mismatch deep in the call tree would trigger polymorphic selection deep below in the call stack. I don't think anyone apart from myself was ever capable or willing to spelunk the reification logs to determine cause and effect for some of the most astonishing endcomes.

With an increasing focus on user experience and approachability of the language, I started to chip away at the overpowered default behavior.

Manual Sanity Checks

One of the first things that became painfully obvious is the fact that the reification of a function parameter should usually not influence the higher order function that calls it.

Let's explore how things go wrong in a simulation of the way primal Kronos used to work.

; just ignore me while I defeat some sanity checks
Dangerous-Eval(fn args) #[Pattern] {	
	val = Handle(fn(args) { nil })
	When(Not(Nil?(val)) val)
}

; by itself, this seems like a reasonable implementation of fold.
Dangerous-Fold(fn values...) {
	; terminating case when 'values...' can't be split any more
	Dangerous-Fold = values...

	(x xs) = values...
	Dangerous-Fold = Dangerous-Eval(fn x Recur(fn xs))
}

Dangerous-Fold(Add 1 2 3)6

Now consider a type failure in fn:

Dangerous-Fold(Add 1 2 "foo")1 2 foo

This is clearly nonsensical. The result is because reification of Add(2 "foo") wasn't legal, and caused Dangerous-Fold to fall back to the case we intended as terminating. However, values... wasn't an atom but bound to (2 "foo"). Next Kronos tries to Add(1 2 "foo") with no better luck, and bails to the outer terminating path.

The sanity checks in the modern version nip this in the bud:

Better-Fold(fn values...) {
	Better-Fold = values...
	(x xs) = values...
	Better-Fold = fn(x Recur(fn xs))
}

Better-Fold(Add 1 2 3)6

Better-Fold(Add 1 2 "foo")
* E-9995: Fatal{Eval (Anon-Fn nil) Fatal{eval nil Fatal{Better-Fold (:Fn{:Add} Floatx2 foo) Fatal{Recur <<(:Fn{:Add} Float foo)>> Fatal{fn (Float <<foo>>) Fatal{:Fallback:Binary-Op (:Fn{:Add} Add Float <<foo>>) Fatal{:Fallback:No-Match (Add Float <<foo>>) Exception{Type mismatch{Could not find a valid form of ' Add ' for arguments of type ' (Float foo) '}}}}}}}}}

| Better-Fold(<<(:Fn{:Add} Floatx2 ... )
|  Recur(<<(:Fn{:Add} Float f ... )
|    fn(Float <<foo>>)
Cannot 'Add' these types at compile time
Received (Float <<foo>>)

Cannot 'Add' these types natively
Received <<foo>>

|      :Fallback:Binary-Op(:Fn{:Add} Add Float ... )
|         Coerce-Binary(Float <<foo>>)
|           Type-Conversion:Implicit(<<foo>> Float)
No match
 in C:\ProgramData\Kronos\Cache\kronoslang\core\0.12.9\Implicit-Coerce.k(8;19)
	Coerce-Binary = (Type-Conversion:Implicit(b a) b)
	                 ^^^

|           Type-Conversion:Implicit(Float <<foo>>)
No match
 in C:\ProgramData\Kronos\Cache\kronoslang\core\0.12.9\Implicit-Coerce.k(7;21)
	Coerce-Binary = (a Type-Conversion:Implicit(a b))
	                   ^^^

No match
 in C:\ProgramData\Kronos\Cache\kronoslang\core\0.12.9\Implicit-Coerce.k(15;10)
	func(Coerce-Binary(a b))
	     ^^^

|        :Fallback:No-Match(Add Float <<foo>>)
Could not find a valid form of ' Add ' for arguments of type ' (Float foo) ' (Type mismatch)
Received (Add Float <<foo>>)

We still get a scary message, but at least the compiler explains how it tried to implicitly convert values to conform, and refuses to descend further into madness.

Moral: propagating specialization failure is powerful and should be explicit. That's why in contemporary kronoslang we need to introduce it via the #[Pattern] attribute, like we did with Dangerous-Eval to make it behave irresponsibly.

Introducing Gradual Typing

Kronos is a compile-time circuit generator with a Turing-complete type system. That design can be critiqued as resulting in some volatile, explosive tendencies. Like C++ templates, it is a bit like a dynamically typed program that generates a statically typed program. The usability problem here is that the manifestation of an error is rarely proximate to its cause.

The rest of this article demonstrates a new feature in Kronos compiler series 0.14+ that draws inspiration from C++ concepts and clojure.spec, helping to localize errors and bail early when a type branch makes no sense.

Improving on Manual Type-Checking

We have had compile-time reflection for a long time, and I recently introduced constraints to help building polymorphic patches visually in Veneer.

Real?(1)True


Real?("foo")nil


Constraints:Real!(1)1


Constraints:Real!("foo")
* E-9995: #Specialization failure

| Constraints:Real!(foo)
No match

Constraints have the #[Pattern] matching attribute by convention, and thus influence form selection for the function that calls them:

Describe(x) {
	Use Constraints

	Describe = 
		("sequence:" 
			Algorithm:Map(
				Describe Sequence!(x)))

	Describe = ("some number" Real!(x))
	Describe = ("integer" Integer!(x))
	Describe = ("compile-time constant" Constant!(x))
}

Describe(1)some number 1

Describe(#42)compile-time constant #42

Describe(1 2q #3 (#4 5) 6)sequence: (some number 1) (integer 2) (compile-time constant #3) (sequence: (compile-time constant #4) some number 5) some number 6

Sugared Constraints

The first new feature is a handy shorthand for adding type constraints to symbol binding:

foo:Real! = 3
foo3


bar:Real! = "not real"
bar
* E-9995: #Specialization failure

Type of 'bar' must match 'Real!'
Received not real

This can be used for function arguments as well.

Hypot(a:Real! b:Real!) {
	Math:Sqrt(a * a + b * b)
}

Hypot(3 4)5


Hypot(#3 4)5


Hypot(3 "FOUR!")
* E-9995: Fatal{Eval (Anon-Fn nil) Fatal{eval nil Fatal{Hypot (Float FOUR!) Fatal{:Fallback:No-Match (:Hypot Float FOUR!) Exception{Type mismatch{Could not find a valid form of ' :Hypot ' for arguments of type ' (Float FOUR!) '}}}}}}

| Hypot(Float FOUR!)
Type of 'b' must match 'Real!'
Received FOUR!

|  :Fallback:No-Match(:Hypot Float FOUR!)
Could not find a valid form of ' :Hypot ' for arguments of type ' (Float FOUR!) ' (Type mismatch)
Received (:Hypot Float FOUR!)

The error message also got a lot nicer. Note that this kind of precondition checking is optional, and can be used selectively, even within a single expression.

We've decorated some library functions with useful constraints:

Algorithm:Expand(#10 (+ 1) 1)1 2 3 4 5 6 7 8 9 10 nil


Algorithm:Expand(10 (+ 1) 1)
* E-9995: Fatal{Eval (Anon-Fn nil) Fatal{eval nil Fatal{Algorithm:Expand <<(Float :Fn{} Float)>> Fatal{:Fallback:No-Match (:Algorithm:Expand <<Float :Fn{} Float>>) Exception{Type mismatch{Could not find a valid form of ' :Algorithm:Expand ' for arguments of type ' (Float :Fn{} Float) '}}}}}}

| Algorithm:Expand(<<(Float :Fn{} Float ... )
Type of 'count' must match 'Constant!'
 in C:\ProgramData\Kronos\Cache\kronoslang\core\0.12.9\Algorithm.k(9;1)
	Expand(count:Constant! iterator seed) {
	^^^
Received Float

|  :Fallback:No-Match(:Algorithm:Expand < ... )
Could not find a valid form of ' :Algorithm:Expand ' for arguments of type ' (Float :Fn{} Float) ' (Type mismatch)
 in C:\ProgramData\Kronos\Cache\kronoslang\core\0.12.9\Algorithm.k(9;1)
	Expand(count:Constant! iterator seed) {
	^^^
Received (:Algorithm:Expand <<Float :Fn{} Float>>)

Sugared Type Declarations

Finally, there's additional syntax to declare nominal types with a canonical structure. Let's see how we could use it to implement a subset of complex arithmetic.

First, this is how we would do it in the old manual way:

Type Old-Complex

re = 1
im = 1

; manually decorate a pair with a type tag
z = Make(Old-Complex re im)
i = Make(Old-Complex 0 1)

; extend `Mul` for our custom type
Mul(a b) #[Extend] {
	; `Break` pattern matches by default
	(ar ai) = Break(Old-Complex a)
	(br bi) = Break(Old-Complex b)

	Make(Old-Complex 
			ar * br - ai * bi 
			ar * bi + br * ai)
}

z{Old-Complex 1 1}


i{Old-Complex 0 1}


z * i{Old-Complex -1 1}

Of course, it would make sense to wrap it in packages and constructor functions to make using it less error-prone - as is, we allow anything to go into the real and imaginary parts, including strings, vectors, closures or other complex numbers.

New Type Syntax

Or we could use the new sugar, which generates constructors, accessors and type constraints from a single directive.

; declare our type with constrained members
Type New-Complex(Real:Real! Img:Real!)

Mul(a b) #[Extend] {
	; Generated accessors are in :New-Complex
	Use New-Complex
	
	Cons(
		Real(a) * Real(b) - Img(a) * Img(b)
		Real(a) * Img(b)  + Img(a) * Real(b))
}

; constructor argument order mirrors the type declaration
z* = New-Complex:Cons(1 1)
i* = New-Complex:Cons(0 1)

; we get early type checking
New-Complex:Cons("not really" "a number")
* E-9995: Fatal{Eval (Anon-Fn nil) Fatal{eval nil Fatal{New-Complex:Cons (not really a number) Exception{Fatal{Invalid constituent types for nominal `:New-Complex(real img)`}}}}}

| New-Complex:Cons(not really a number ... )
Type of 'Img' must match 'Real!'
Received a number

Invalid constituent types for nominal `:New-Complex(real img)` (Fatal)
Received (not really a number)




; we get constrained accessor functions
New-Complex:Real(z*)1

New-Complex:Img("this string has no real or imaginary parts")
* E-9995: #Specialization failure

| New-Complex:Img(this string has no r ... )
Cannot destructure as a nominal type `:New-Complex`
Received this string has no real or imaginary parts
Expected #:New-Complex




; we get automatic reflection and constraints
New-Complex?(z*)True

New-Complex?(42)nil


Constraints:New-Complex!(z*){New-Complex 1 1}

Constraints:New-Complex!(1)
* E-9995: #Specialization failure

| Constraints:New-Complex!(Float)



z* * i*{New-Complex -1 1}

We can further make use of the constraints the compiler generates in our new functions.

Conjugate(x:Real!) {
	x
}

; add alternative forms with #[Extend]
Conjugate(z:New-Complex!) #[Extend] {
	Use New-Complex
	Cons(Real(z) Neg(Img(z)))
}

Conjugate(z*){New-Complex 1 -1}


Conjugate(5)5

Type constraints yield a natural way to extend functions already present in the standard library.

Abs(z:New-Complex!) #[Extend] {
	Use New-Complex
	Math:Sqrt(Real(z * Conjugate(z)))
}

Abs(z*)1.4142135


; because of type constraints, we did not break the pre-existing `Abs`
Abs(-3)3

This concludes the demonstration of gradual typing features introduced in Kronos. Please feel free to give your feedback or explore the feature with the most recent releases of the native compiler!