Sugar for anonymous tuples and projecting away type parameters

[kris-brown]

It would be nice to have anonymous tuples as well as the ability to project away type parameter information. These came up for me as I tried to do a 'simple' example of showing that a theory of vectors was a monoid via a theory morphism. This requires sending default::TYPE to some type in ThVect. However, if one only is able to say Vect(n) for some n, then there doesn't exist a type for default to get mapped to!

using GATlab, GATlab.Stdlib

"""
A theory of vectors with elements of type `X` and type-level length information,
e.g. given a model with `X` mapping to `Symbol`, then [:a,:b,:c] is a Vect(3).

This has the intended semantics if ℕ really is the natural numbers, but this 
would require a doctrine that can express sum types, which GATs cannot.
"""
@theory ThVect <: ThNatPlus begin
  #########
  # Types #
  #########
  X::TYPE
  Vect(len::ℕ)::TYPE

  #######################################################################
  # Ability to forget/recover type information: should be autogenerated #
  #######################################################################

  Vect::TYPE # type of all vects, of any length. In bijection with ΣₙVect(n)
  len(v::Vect)::ℕ


  πVect(v::Vect(n))::Vect ⊣ [n::ℕ]
  ιVect(v::Vect)::Vect(len(v)) 

  len(πVect(v)) == n ⊣ [n::ℕ, v::Vect(n)]

  ιVect(πVect(v)) == v ⊣ [n::ℕ, v::Vect(n)]
  πVect(ιVect(v)) == v ⊣ [v::Vect]

  ###################################################
  # Ability to tuple types: should be autogenerated #
  ###################################################

  X_Vect(n::ℕ)::TYPE # type of (X,Vect(n)) pairs
  mk_tup(x::X, v::Vect(n))::X_Vect(n) ⊣ [n::ℕ] 
  proj1(xv::X_Vect(n))::X ⊣ [n::ℕ] 
  proj2(xv::X_Vect(n))::Vect(n) ⊣ [n::ℕ] 

  proj1(mk_tup(x,y)) == x ⊣ [n::ℕ, x::X, y::Vect(n)]
  proj2(mk_tup(x,y)) == y ⊣ [n::ℕ, x::X, y::Vect(n)]

  ##############
  # Operations #
  ##############

  empty()::Vect(Z())
  concat(x::Vect(n), y::Vect(m))::Vect(n+m) ⊣ [(n,m)::ℕ]
  pop(v::Vect(S(n)))::X_Vect(n) ⊣ [n::ℕ]
  push(x::X, v::Vect(n))::Vect(S(n)) ⊣ [n::ℕ]

  proj2(pop(push(x, v))) == v ⊣ [x::X, n::ℕ, v::Vect(n)]
  
  concat(v, push(x,w)) == push(x, concat(v,w)) ⊣ [
    (n,m)::ℕ,v::Vect(n),w::Vect(m), x::X] # push goes to end of list

end

@theorymap F(ThMonoid, ThVect) begin
  default() => Vect
  e() => πVect(empty())
  (a⋅b) ⊣ [(a,b)::default] => πVect(concat(ιVect(a),ιVect(b))) 
end

This is in the spirit of struct type sugar, which has very basic support (see NonStdlib's ThPushout),

[kris-brown]

If this sugar existed, my example might look like this (comments point out the differences from above)

@theory ThVect <: ThNatPlus begin
  X::TYPE
  Vect(len::ℕ)::TYPE

  empty()::Vect(Z())
  concat(x::Vect(n), y::Vect(m))::Vect(n+m) ⊣ [(n,m)::ℕ]
  pop(v::Vect(S(n)))::(X, Vect(n)) ⊣ [n::ℕ] # NOTE: the tuple syntax
  push(x::X, v::Vect(n))::Vect(S(n)) ⊣ [n::ℕ]

  pop(push(x, v))[2] == v ⊣ [x::X, n::ℕ, v::Vect(n)] # NOTE: the [index] syntax
  
  concat(v, push(x,w)) == push(x, concat(v,w)) ⊣ [
    (n,m)::ℕ,v::Vect(n),w::Vect(m), x::X] 

end

@theorymap F(ThMonoid, ThVect) begin
  default() => Vect # NOTE we should automatically be able to refer to `Vect`
  e() => empty()
  (a⋅b) ⊣ [(a,b)::default] => concat(a,b) # NOTE: the π/ι casting should be automatic
end