I’ve taken to commenting the closing brace of my inner dfns with a home-grown type notation pinched from the Functional Programming community:

    dref←{                  ⍝ Value for name ⍵ in dictionary ⍺ 
        names values←⍺      ⍝ dictionary pair
        (names⍳⊂⍵)⊃values   ⍝ value corresponding to name ⍵
    }                       ⍝ :: Value ← Dict ∇ Name

I keep changing my mind about whether the result type should be to the left (Value ← ...) or to the right (... → Value). The FP crowd favours → Value but I’m coming around to Value ← because:

* In contrast to (say) Haskell, APL’s function/argument sequences associate right.
* Value ← mirrors the result pattern in a tradfn header and so looks familiar.
* The type of function composition f∘g is simpler this way round.

Such comments serve as an aide-mémoire when I later come to read the code though, with some ingenuity, the notation might possibly be extended to a more formal system, which could have value to a compiler or code-checker. We would need:

Glyphs for Dyalog’s three primitive atomic data types. For no particularly good reason, I’ve been using:

# number
' character
. ref

Glyphs for a few generic (polymorphic) types. These could be just regular lower-case letters a b c … though I currently prefer greek letters:

⍺ ∊ ⍳ ⍴ ⍵ ...


Some constructors for type expressions. This is the most contentious part. For what it’s worth, I’ve been using:

::  is of type ...
∇  function
∇∇  operator
←  returns
[⍺] vector of ⍺s
{⍺} optional left argument ⍺

For example:

foo :: ⍵ ← {⍺} ∇ ⍵

implies:
– foo is an ambi-valent function whose
– result is of the same type (⍵) as its right argument and whose
– optional left argument may be of a different type (⍺).

I can abstract/name type expressions with (capitalised) identifiers using :=. For example:

Dict   := [Name][Value]        ⍝ dictionary name and value vectors
Eval   := Expr ← Dict ∇ Expr   ⍝ expression reduction
List ⍵ := '∘' | ⍵ (List ⍵)     ⍝ recursive pairs. See list
Name   := ⍞                    ⍝ primitive type: character vector

The type: character vector ['] is used so frequently that the three glyphs fuse into: ⍞. This means that a vector-of-character-vectors, also a common type, is [⍞].

Primitive and derived function types.
If we’re not too nit-picky and ignore issues such as single extension and rank conformability, we can give at least hints for the types of some primitive functions and operators.

 ⍳ :: # ← ⍺ ∇ ⍺              ⍝ dyadic index-of
 ⍴ :: ⍺ ← [#] ∇ ⍺            ⍝ reshape (also take, transpose, ...)

The three forms of primitive composition have interesting types:

∘ :: ⍴ ← {⍺} (⍴ ← {⍺} ∇ ⍳) ∇∇ (⍳ ← ∇ ⍵ ) ⍵     ⍝ {⍺}f∘g ⍵
:: ⍴ ←                 ⍺ ∇∇ (⍴ ← ⍺ ∇ ⍵ ) ⍵   ⍝ A∘g ⍵
:: ⍴ ←      ((⍴ ← ⍺ ∇ ⍵) ∇∇ ⍵ )⍺             ⍝ (f∘B)⍵

It follows that:

f :: ⍴ ← {⍺} ∇ ⍳
g :: ⍳ ←     ∇ ⍵
=> f∘g :: ⍴ ← {⍺} ∇ ⍵          ⍝ intermediate type ⍳ cancels out

and for trains:

A :: ⍳                  ⍝ A is an array of type ⍳
f :: ⍳ ← {⍺} ∇ ⍵
g :: ⍴ ← {⍳} ∇ ∊
h :: ∊ ← {⍺} ∇ ⍵
=> f g h :: ⍴ ← {⍺} ∇ ⍵        ⍝ fgh fork
=> A g h :: ⍴ ←     ∇ ⍵        ⍝ Agh fork
=>   g h :: ⍴ ← {⍺} ∇ ⍵        ⍝ gh atop

For a more substantial example, search function joy for :: and := in a recent download of dfns.dws.

Muse:
This notation is not yet complete or rigorous enough to be of much use to a compiler but there may already be enough to allow the writing of a dfn, which checks its own and others internal consistency. In the long term, if a notation similar to this evolved into something useful, it might be attractive to allow optional type specification as part of the function definition: without the comment symbol:

    dref←{                  ⍝ Value for name ⍵ in dictionary ⍺ 
        names values←⍺      ⍝ dictionary pair
        (names⍳⊂⍵)⊃values   ⍝ value corresponding to name ⍵
    } :: Value ← Dict ∇ Name

Follow