As I wrote about previously I am working on a typed array language with the case of elliptic Fourier series as an example.

The compiler now works so I present the correct version:

λxs.λys.
{ sum ← [(+)/1 0 x]
; tieSelf ← [({.x)⊳x]; Δ ← [(-)\~(tieSelf x)]
; dxs ⟜ Δ xs; dys ⟜ Δ ys
; dts ⟜ [√(x^2+y^2)]dxs dys
; pxs ← (+)Λ dxs; pys ← (+)Λ dys; pts ⟜ (+)Λ dts
; dtss ⟜ (-)\~((^2)'1 (0<|pts))
; T ⟜}. pts
; 𝜉 ← (-)pxs ((*)((%)dxs dts) pts)
; 𝛿 ← (-)pys ((*)((%)dys dts) pts)
; A ← ((sum ((*)((%)dxs dts) dtss))%2 + (sum ((*)𝜉 dts)))%T
; C ← ((sum ((*)((%)dys dts) dtss))%2 + (sum ((*)𝛿 dts)))%T
; (A,C)
}

This is shockingly close to what I wrote with only the typechecker working:

λxs.λys.
{ sum ⇐ [(+)/1 0 x]
; dxs ⟜ (-)\~xs; dys ⟜ (-)\~ys
; dts ⟜ [√(x^2+y^2)]dxs dys
; pxs ← (+)Λₒ 0 dxs; pys ← (+)Λₒ 0 dys; pts ⟜ (+)Λₒ 0 dts
; dtss ⟜ 0<|(-)\~((^2)'1 pts)
; T ⟜}.pts
; 𝜉 ← (-)pxs ((*)((%)dxs dts) pts)
; 𝛿 ← (-)pys ((*)((%)dys dts) pts)
; A ← ((sum ((*)((%)dxs dts) dtss))%2 + (sum ((*)𝜉 dts)))%T
; C ← ((sum ((*)((%)dys dts) dtss))%2 + (sum ((*)𝛿 dts)))%T
; (A,C)
}

I believe this shows the promise of typing arrays: static typing offers faster feedback and even more incisive errors (being more abstract, they get to the heart of the matter).

A further advantage: Apple infers types and thus we do not need to write redundant documentation.