Arrays?

[echatav]

I'm a little confused by Postgres arrays. From the documentation:

However, the current implementation ignores any supplied array size limits, i.e., the behavior is the same as for arrays of unspecified length.

The current implementation does not enforce the declared number of dimensions either. Arrays of a particular element type are all considered to be of the same type, regardless of size or number of dimensions. So, declaring the array size or number of dimensions in CREATE TABLE is simply documentation; it does not affect run-time behavior.

But also,

Multidimensional arrays must have matching extents for each dimension. A mismatch causes an error.

What I've been thinking is that Squeal should not support nested arrays, but rather, single-dimensional variable length arrays and multidimensional static length arrays, over nullity types, something like

data PGType
  = ..
  | PGvararray NullityType
  | PGfixarray [Nat] NullityType

Then the actual type expressions should restrict users from expressing nested arrays (i.e. no vararray (vararray int)s) or 0-dimensional arrays (i.e. no fixarray @'[] ints). Does this make sense? Is there a better way to do arrays?

[mikeplus64]

My understanding is, what Postgres supports is:

(where any must also satisfy the rules below...)

1. any[?N][?M], where inner arrays must all have the same length, which is checked, but Postgres does not check that the length is actually N; it only matters to Postgres that the lengths are consistent, not that they match the length N, if it was specified at all. If M is given it is also not checked at all.

2. any[?M], where M is not checked at all at runtime.

There's nothing particularly wrong with 0-dimensional arrays, although they're probably not useful.

More succinctly: the outermost array can have any dimension, or none at all. At each level of nested array, the arrays at that level must have the same length.

So nested arrays only being valid for 'PGfixarray n (nullity ('PGfixarray m ty)) and PGvararray (nullity ('PGfixarray m ty) sounds fine to me. I'd strongly prefer the constraint being expressed in PGType itself or else we have yet another constraint to carry around. With the help of TypeInType it should be possible by giving PGType a parameter to "narrow" valid sub-types, and expressing it as a GADT...

[mikeplus64]

>>> data K = T | V K | F K
>>> data P :: K -> Type where PT :: P t; PV :: (forall k. P k) -> P ('V k); PF :: (forall k. P k) -> P t
>>> :kind! ('PF ('PV 'PT))

<interactive>:1:7: error:
    • Expected kind ‘forall (k :: K). P k’,
        but ‘ 'PV  'PT’ has kind ‘P ('V k0)’
    • In the first argument of ‘ 'PF’, namely ‘( 'PV  'PT)’
      In the type ‘( 'PF ( 'PV  'PT))’
-- good
>>> :kind! ('PF 'PT)
('PF 'PT) :: P t
-- also good
>>> :kind! ('PV ('PF 'PT))

<interactive>:1:7: error:
    • Expected kind ‘forall (k :: K). P k’,
        but ‘ 'PF  'PT’ has kind ‘P t0’
    • In the first argument of ‘ 'PV’, namely ‘( 'PF  'PT)’
      In the type ‘( 'PV ( 'PF  'PT))’

-- huh? the line above says ('PF 'PT) :: P t. ???

I thought that should work. I don't understand why the last error occurs.

[echatav]

Interesting. So there's a pretty good reason to disallow any nested arrays, if we want to play well with nullability. You get a dimension mismatch error if you try to construct an array of type 'PGvararray ('Null ('PGfixarray 2 'PGint4)).

> VALUES (ARRAY[NULL, ARRAY[1,2]] :: int4[2][]);
multidimensional arrays must have array expressions with matching dimensions

So, the base elements of the array can be null but not any intermediate elements. This is sort of evidenced when you look into the Postgres catalog tables to see how type information is stored. Array types have a base type which itself cannot be an array type.

Another consideration here is reusing the array decoding and encoding work from postgresql-binary, which I'd like to do if possible.

I'd strongly prefer the constraint being expressed in PGType itself or else we have yet another constraint to carry around.

Even without generalized algebraic datakinds, we can still express the invariant at the type level:

data BaseType = 'PGint4 | ..
data PGType = BaseType BaseType | PGvararray BaseType | PGfixarray [Nat] BaseType

I kind of didn't want to do that because it would make the type level DSL more complicated with a bunch of 'BaseTypes clutter.

More succinctly: the outermost array can have any dimension, or none at all. At each level of nested array, the arrays at that level must have the same length.

Totally, the outermost array need not worry about mismatching dimensions. So maybe something like

data Dim = Var | Fix Nat
data PGType = BaseType BaseType | PGarray [Nat] Dim BaseType

This would capture exactly what's allowable (I think) though I'd still rather avoid splitting up PGType into base types and array types. Carrying around a constraint seems unavoidable, at the very least the Nats must be KnownNats.

[echatav]

Ack, I forgot about nullability which screws up splitting even more, we'd need nullable base types and nullable pgtypes.

[echatav]

So how about we have

data PGType
  = 'PGbool
  | 'PGint4
  | ..
  | 'PGarray [Nat] Dim NullityType

data NullityType = Null PGType | NotNull PGType

data Dim = Var | Fix Nat

And then 3 type expression constructors, vararray, and fixarray for single-dimensional arrays and multiarray for multi-dimensional arrays?

[echatav]

Relevant documentation, note that types themselves are typed

typtype is b for a base type, c for a composite type (e.g., a table's row type), d for a domain, e for an enum type, p for a pseudo-type, or r for a range type. See also typrelid and typbasetype.

The closer we match the system catalog, the better we'll be able to integrate down the line when we add multi-schema support and schema verification.

[echatav]

Or better yet, we could allow nesting array type expression constructors by using a type family and clever constraints to calculate the correct 'PGarray inners outer base, then we'd only need the fixarray and vararray constructors as we now have.

[echatav]

done in 0.4