blog

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.