On Mon, Apr 6, 2015 at 3:46 PM, Justin R. Slepak <[email protected]> wrote:
...(though I've clipped out a lot)...
> Adding recursive types lets us, for example, define singly-linked lists of
> integers
> as, "a LinkedList is either (sum type!) Empty or a tuple (product!) with a
> Integer
> and another LinkedList." (Empty is just some designated special value here).
> Now
> we have the ability to use one type to describe sequences of any length.
Note that Integers themselves might be thought of as sequences of any
length and/or as recursive types.
Practically speaking, of course, "any length" is a lie - it's a
deliberate ignoring of machine constraints.
But it's a traditional and sometimes useful lie. (Though of course
sometimes it's a problem we have to deal with.)
Anyways, in some languages (including J) we have both a fixed width
integer type which is used for most practical problems and an
arbitrary width integer type which is used for a different class of
problems.
> We can also have terms and types that are parameterized over other types
> ("parametric polymorphism" and "higher-kinded types"... or simply "generics").
> Now we can make our LinkedList definition handle any element type:
> "a LinkedList<T> is either Empty or a tuple with a T and another
> LinkedList<T>."
> Now `LinkedList` itself is like a function, but at the type level. Its input
> is a type
> (perhaps Float), and it's output is a type (LinkedList<Float>).
"Like a function" sort of begs the question, it's the sort of
abstraction you get when
you implement against a higher level language. And that can leave you
with either
a temporary system (as you bootstrap yourself into using your target language as
your host language) or a permanent kludge (where you never actually deal with
the underlying machine).
Meanwhile, market forces push heavily in the direction of temporary
kludges (which are great if you just want to get out of your job and
go do something else instead).
It's not that this is wrong, but it relates to a point I want to make
further down. I'll mark that with ***
> First, how do we talk about what we can *do* with arrays?
>
> We have a few options for ascribing types to arrays (which will specify how
> they
> can be used), and they'll give us differing levels of safety guarantee but
> also differing
> levels of complexity to implement and use.
Note that at least some common concepts of "safety" correspond
strongly with "simplicity".
> 1. All arrays of a given element type have the same type (Array<E>). It's
> easy to
> describe the behavior of a function/verb when you only need to state what
> type of
> elements its arguments and results should have (and you can always write a
> verb
> whose result shape is "too dynamic"). On the other hand, we get no guarantee
> about
> having shape-matched arguments. `1 2 3 + i. 2 2` would have no type error.
In other words: treat the array as being arbitrarily large and
prefixed with arbitrarily many ones for unspecified dimensions and
filled with arbitrarily many zeros for unspecified elements.
Some time it might be fun to play around with an implementation like
this, despite its obvious problems.
> 2. All arrays of a given element type *and rank* have the same type.
> This is a sensible enough plan for languages without J's implicit operator
> lifting. There are a couple ways we could do it:
> 2a. Describe arrays with a Vector<E> type, where E is a scalar, Vector<E>
> has rank 1, Vector<Vector<E>> has rank 2, etc. It fits nicely with the type
> theory we have, but it's hard to describe the behavior of some functions that
> change the rank of their input (our "language" of rank behavior is limited to
> adding or subtracting a constant).
> 2b. The type for a rank-N array of E is Array<N,E>. This calls for somewhat
> more complicated type theory: we need to have types parameterized over terms
> ("dependent types") or at least have a "type-level" version of natural
> numbers.
Note that J's arrays (of a specific element type) are perhaps best described as:
Vector<Vector<N>>
This is different from your Vector<Vector<E>> in that N is the rank of
the array, instead of 2 being the rank of the array.
*** However, this mode of expression does fit your "Like a function"
concept for types. ***
If we allow ourselves a step away from the completely abstract and
into the practical, consider:
i.5 7 11
Here, the rank of the array is 3. So that's N.
Here, Vector<3> takes the value 5 7 11
And, here, Vector<5 7 11> takes the value produced by i.5 7 11.
Of course, what this means is that given a scalar argument, Vector<N>
gives us a vector, and given a vector argument, Vector<XYZ> gives us
an array.
But since we've made a point of abandoning any concrete representation
(my "enumeration of possibilities") and gone with an abstraction (your
"like a function"), I feel that it's fair if I take a direct route to
the goal.
But of course this does leave us needing an intermediate "bootstrap
type system" that lets us define a Vector<> which has at least two
separate implementations. And it might be clearer if we gave each of
those implementations a different name?
> 3. All arrays of a given element type and *shape* have the same type.
As you point out, this leads to high complexity when dealing with
boxed arrays. Though I suppose the other concepts have similar (albeit
perhaps simpler) problems with them?
...[much elided]...
> There's enough existing code, expectation, intuition, idiom, etc. which would
> break that I don't think J itself should try to integrate type theory.
Agreed.
Though I do see some promise for an ML-style type system subset of J as an
alternative to having to build code in some external language when dealing with
extremely scalar algorithms which have somehow managed to become performance
critical.
> That said, the prefix-agreement and implicit operator lifting is the piece of
> dynamism I
> really care about in J, and I have found mainstream type theory a convenient
> enough
> way to identify that behavior statically.
I hope it serves you well.
--
Raul
----------------------------------------------------------------------
For information about J forums see http://www.jsoftware.com/forums.htm
