Array type

[byorgey]

The language should also have a type for (size-indexed?) multidimensional arrays. e.g. you could imagine some kind of high-powered sensor device that would return a 2D array of the robot's surroundings, allowing it to do things like pathfinding.

There's a lot of language design to be done here; this issue is something of a placeholder. Should they be mutable? Immutable? What kinds of operations should they support? Should the type of an array reflect its dimension? Its size along each dimension? etc.?

[xsebek]

We already have immutable fixed-size arrays. The trick to getting an array of size n is to use an n+1 tuple:

• base case:

  def get1 : (a * b) -> a
      = fst
  end
  def set1 : x -> (a * b) -> (x * b) 
      = \x.\t. x,snd t
  end

• inductive case (imagine n+1 in place of 2 and missing type annotations):

  def get2 : (a * b * c) -> b
     = \t. let in1 = snd t in fst in1
  end
  def set2 : x -> (a * b * c) -> (a * x * c) 
      = \x.\t. let in1 = snd t in fst t,set1 x in1
  end

• after that we can get all n by induction:

  def get3 : (a * b * c * d) -> c
      = \t. let in1 = snd t in get2 in1
  end
  def set3 : x -> (a * b * c * d) -> (a * b * x * d) 
      = \x.\t. let in1 = snd t in fst t,set2 x in1
  end

• so to get an array with 1,2,3 do:

  > (1,2,3,())
  (1, (2, (3, ()))) : int * int * int * ()
  > get3 (1,2,3,())
  3 : int
  > set3 42 (1,2,3,())
  (1, (2, (42, ()))) : int * int * int * ()

OK, I admit this does not look great, even though we could auto-generate all the definitions with Bash.
I think the way to make this more usable, would be to add type synonyms like we have def, but I can not imagine how hard or easy that would be. (EDIT: I made #153 for this related improvement)
Thoughts, @byorgey?

[byorgey]

Hi @xsebek , yes, good observation! This is definitely a nice way to get yourself fixed-sized, immutable arrays if all you have is pairs, and if players want to do this, by all means they should!

However, this would be unsatisfactory as the "blessed" way to have arrays, for several reasons:

1. It is slow. I expect anything called an "array" to give me O(1) random access to any index, but this encoding with pairs takes linear time to access or update a particular index, because of the need to call snd repeatedly. (It is the same reason that (!!) takes linear time in Haskell.)
2. There is no way to write functions that are polymorphic in the array size. Actually your get and set functions are somewhat polymorphic, because e.g. get3 will work on any 3-tuple or higher. But using your scheme there would be no way, for example, to write a function like mapArray : (a -> b) -> array n a -> array n b that works for any size array.

After thinking about a few use cases (e.g. incrementally building a map while exploring an area), I am also convinced that we need to provide mutable arrays.

[xsebek]

A more determined player could write getXfromY function for each logarithmic encoding ((...*...)*(...)). 🤔
But functions like map could only be written with a fixed number of elements (so mapFirst3,...) which is indeed disappointing. 😞

I am kind of scared by mutable arrays in Haskell, even using ticks to update could lead to weird things if the array was shared between robots (which one gets to update first?).

I think we could get reasonable safety with #94 - say one robot has the array and others ask him to update and what the value is somewhere. With #154 I could write data.intmap.sw, which might be a good pure alternative if mutable arrays turn out to be difficult to share between robots. But maybe I just lack imagination and mutable arrays are in fact easy 🙂

[byorgey]

Well, I agree that using mutable arrays can be scary. But implementing them is easy. I don't think we shouldn't provide a feature just because users can shoot themselves in the foot with it.

If a mutable array is shared and multiple robots try to write to it at the same time, we will just say it is undefined which one gets to update first. That's no different than the situation with shared mutable variables in any other language, of course (Rust excepted, perhaps). Maybe down the road we could provide some kind of atomic compare-and-swap primitive or something so users can implement their own semaphores.

Do I hope players will discover some of the joys of functional programming through playing this game? Yes, of course. But at the same time I'm not trying to force them into any one paradigm.

I think we could get reasonable safety with #94 - say one robot has the array and others ask him to update and what the value is somewhere. With #154 I could write data.intmap.sw, which might be a good pure alternative if mutable arrays turn out to be difficult to share between robots.

These are all great ideas, but it seems like they relate to choices you can make as a player in terms of how to organize your code. I don't think it affects whether we should provide certain features or not.

[byorgey]

A few thoughts:

• The type of an array should reflect whether it is mutable or immutable; the number of dimensions; and the element type.
• I don't think making the actual size along each dimension part of the type is a good idea, since it would require dependent types to declare arrays with a dynamically determined size, and ensuring that array accesses are valid requires arbitrary SMT solving.
• Rather than providing mutable arrays as a primitive thing, another thing to consider might be just providing mutable references as a primitive, and then one can just make an (immutable) array full of mutable references. This might have some implications for efficiency if it's done naively (extra boxing, etc.) but that could be addressed via optimizations.

[byorgey]

I think we should implement immutable arrays as a start. Once we get some experience with those we can think about how to add mutable arrays. As a concrete proposal:

• array a is the type of one-dimensional arrays with elements of type a.
  • n-dimensional arrays can be created by nesting this type.
• For constructing arrays, a primitive built-in function generate : int -> (int -> a) -> array a.
• For accessing arrays, a primitive built-in operator ! which takes an array a and an int and returns an a (and can throw an out-of-bounds exception).
• A built-in function size : array a -> int.
• There are lots of other functions one might want, e.g. map, but those can be implemented in terms of the above. For example,

  mapA : (a -> b) -> array a -> array b
  mapA f arr = generate (size arr) (\i. f (arr ! i))
  

We can certainly think about adding other construction methods. For example, using generate is unsatisfactory for converting a list to an array:

arrayFromList : list a -> array a
arrayFromList as = generate (length as) (\i -> as !! i)

This is unsatisfactory because it takes time quadratic in the length of the list. So we might contemplate providing a primitive function to build an array from a list, with a type like

arrayFromList : (rec l. Unit + a * l) -> Array a

which could probably reuse some of the underlying CESK machine infrastructure for collecting up array values and then creating an array.