Define head, tail, last with patterns, or expose the list selector with type index?

[yav]

Currently they are defined with indexing, but it might be nicer to just use pattern matching, for example like this:

head ([x] # _) = x
tail ([_] # xs) = xs
last (_ # [x]) = x

This (subjectively) is more elegant, and also avoid the need to specify explicit indexing type. However, we should be a little careful to not affect performance. In particular, it'd be nice to do a few optimizing rewrites. To see why, consider how these patterns are desugared:

last (xs : [n + 1]_) = x
  where
  (as,bs) = splitAt`{n} xs  
  x = list_select`{0} bs // this is an internal selector operator that is currently not exposed but maybe we should expose it.

The first optimization that would be nice to do is to replace splitAt with drop if the first components is not used:

last (xs : [n + 1]_) = x
  where
  bs = drop`{n} xs  
  x = list_select`{0} bs

The next optimization would to notice that bs is only used in one place, and that place is a slector, and selecting from a drop is the same as just selecting a bigger number (list_select{a} (drop{b} xs) = list_select{a+b} xs` to get:

last (xs : [n + 1]_) = list_select`{n} bs

While none of this is particularly complicated, it would require a bit of work. Another option would be to just expose the list selector where the index is a type, which is useful for indexing with constants.