A List is not isomorphic to (component-wise) product

[sassa_nf]

(Background: https://stackoverflow.com/questions/69360027/list-set-should-be-a-sort-but-it-isnt)

So what's the deal with List A = ⊤ + A × List A?

Here's a list of types translated into a product of types:

map : List Set → Set
map [] = ⊤
map (A ∷ t) = A × (map t)

The catch is that (A × ...) is a type, and (A ∷ ...) isn't. Seems to me that List and component-wise product are not the same after all... A little weird.

Maybe it's obvious to some.

Comments

[thedeemon]

I wonder what happens if we translate this into Idris.

[sassa_nf]

In Idris it possibly is even more confusing :)

mmm : List Type -> Type
mmm Nil = ()
mmm (h :: t) = (h, mmm t)

[thedeemon]

and what does the compiler say about it?

[sassa_nf]

tio.run is ok with it - just complained that there is no "main".

But the confusing bit here is that (,) in Idris is used in two contexts, and in this case you have to disambiguate what context this is. In this situation (,) is a type former expression, not construction of a tuple.

Similarly in the original problem statement (_×_) is a type former. Still it takes some effort to see how a list of types can be turned into a tuple type, but not the other way around - can't project individual types out of the tuple to construct a list of types.

[thedeemon]

But in dependent types we have the same language of terms on both sides of ":", there should be no real distinction between constructing a type and constructing a value. This is fine in Idris:
x : fst (swap (23, Int))
x = 42

Even this:
x : let p = (23, Int) in fst (swap p)
x = 42


So I understand why Idris is fine with your code but don't understand why Agda is unhappy. I don't know Agda though.

[sassa_nf]

Agda is also happy with the mmm-like construct. Now, try to express the inverse.

nnn : (xs : List Type) -> mmm xs -> List Type
nnn _ Unit = Nil
nnn (_ :: xs) (h, t) = h :: (nnn xs t)

I don't propose that it has to compile, but that's the thing, essentially: you can pattern-match the pair (you can project the components of the pair with fst and snd), but you can't pattern-match type-former. Can you project type a from (a, b)? How about (a->b)?

Ooh, even better, let's start with something simpler, not the inverse entirely:

nnn : (xs : List Type) -> mmm xs -> List Type
nnn _ Unit = Nil
nnn _ (h, _) = h :: Nil

I get

.code.tio.idr:7:1-3:
  |
7 | nnn _ (h, _) = h :: Nil
  | ~~~
When checking left hand side of nnn:
When checking an application of Main.nnn:
        Type mismatch between
                (A, B) (Type of (h, b))
        and
                mmm xs (Expected type)

[thedeemon]

Don't you just lose information in `List Type -> Type`? Given this type signature, all we know about the result of `mmm xs` is that it's some Type and nothing more. So we can't extract anything. It's not really about lists vs. tuples.

You can still extract `a` from `(a,b)` if you know it's `(a,b)`.

[sassa_nf]

No, it is not the reason. Let's modify mmm:

mmm : List Type -> Type
mmm Nil = ()
mmm (h :: t) = ()

nnn : (xs : List Type) -> mmm xs -> List Type
nnn _ Unit = Nil

Here it can tell that Unit is mmm xs.

Let's pause for a moment. You can extract `a` from `(a, b)`, when `(,)` is the tuple constructor, no doubt about that. But is it a tuple constructor in `mmm (h :: t) = (h, mmm t)`?

[thedeemon]

I'd say yes but I really don't know the mechanics of Idris & Agda well enough to continue.

[sassa_nf]

ok.

My thinking is that in the latter context `(,)` has the same role as `->` - a type former of arity 2. Then `A -> B` is only a way to say "a type corresponding to a pair of types A and B [with the special meaning conferred by _->_ to the entire family of such types]" - but you can't extract A from `A -> B` - in fact, `A` doesn't exist in any form in `A -> B`. In the same manner `A` doesn't exist in `(A, B): Type`, just Idris adds confusion by using `(,)` for both type declaration and instance (de-)construction. In Agda type is declared with `A × B : Set`, and values of that type are constructed as `(a : A , b : B) : A × B`.

My original post was about confusion I noticed in my reasoning - are we in the world of types or in the world of values when we say a List is an n-ary product of all the values in the list; and what world we are in, when the values of the List are types themselves.

[thedeemon]

My point is these are not two distinct worlds (apart from level number in universes hierarchy).