Add sound withFirst and withOnly alternatives to summonFirst and summonOnly

[bplommer]

I think users expect the public API of Shapeless to be type-safe, but summonFirst does a cast that isn't in general correct (e.g. it would happily widen Extract[Some] to Extract[Option]).

I tried to write a sound version but I think it would require Shapeless 2 style typeclass-based dependent typing, so I'm not sure it's worth it.

This doesn't cover K11 and K2 - I'll add them if this is approved in principle.

[joroKr21]

Yeah I noticed that too but I think we should have summonFirst[F, T]: F[?] (apart from withFirst)

[bplommer]

On second thought I'm coming round to the idea of a FirstCoproductInstance type class - it would represent existentially quantified instance availability in a way that's more symmetric with CoproductInstances' representation of universally quantified instance availability. Then e.g. the Empty derivation for coproduction types would require using FirstCoproductInstance, analogously with how the product derivation requires using ProductInstances. It also then wouldn't need to be inline. Wdyt?

[bplommer]

Yeah I noticed that too but I think we should have summonFirst[F, T]: F[?] (apart from withFirst)

Also, it turns out that signature isn't possible in Scala 3 with irreducible existential types being dropped

[joroKr21]

Also, it turns out that signature isn't possible in Scala 3 with irreducible existential types being dropped

Ah I guess that's the reason why there is a cast currently.

On second thought I'm coming round to the idea of a FirstCoproductInstance type class - it would represent existentially quantified instance availability in a way that's more symmetric with CoproductInstances' representation of universally quantified instance availability.

Interesting, I'm not sure what useful methods it would have. And what about FirstProductIntsance?

[milessabin]

IIRC U should be the LUB of the elements of T. At the time I wrote summonFirst it wasn't possible to express that directly, but maybe the situation has changed ... I think we should explore that before trying alternatives. I'm fairly 👎 to using ?.

[joroKr21]

The LUB only works when F is covariant - if it's contravariant it should be GLB

[bplommer]

The LUB only works when F is covariant - if it's contravariant it should be GLB

Exactly - and when it's invariant, as with Empty, there's no sound option.

[milessabin]

and when it's invariant, as with Empty, there's no sound option.

There is a sound option, it's just very constrained.

[bplommer]

There is a sound option, it's just very constrained.

Sorry yes - I meant no sound option without knowing the type for the specific instance. Something like this seems to work but I'm not sure if it justifies the extra complexity:

object FirstCoproductInstance {
  type Aux[F[_], T, U0] = FirstCoproductInstance[F[_], T] { type U = U0}
  
  private transparent inline def derive[F[_], T, T0]: FirstCoproductInstance[F, T] = inline erasedValue[LiftP[F, T0]] match {
    case _: (a *: b) => summonFrom {
      case aa: `a` => new FirstCoproductInstance[F, T] {
        type U = Head[T0]
        val instance: F[U] = aa.asInstanceOf
      }
      case _ => derive[F, T, Tail[T0]]
    }
  }
  transparent inline given[F[_], T](using CoproductGeneric[T]): FirstCoproductInstance[F, T] = derive[F, T, T]
}

def summonFirst[F[_], T](using sf: FirstCoproductInstance[F, T]): F[sf.U] = sf.instance

[bplommer]

Interesting, I'm not sure what useful methods it would have.

probably just withFirst.

And what about FirstProductIntsance?

Actually, I think we'd need that in K1 to derive Extract. We'd want something like def project[T[_], A, R](ta: T[A])(f: [t[_]] => (F[t], t[A]) => R) in order to extract a value from the first element of a product that has an instance.

[joroKr21]

I think we should just emulate an existential with something like

trait Existential[F[_]] {
  type A
  def value: F[A]
}

[joroKr21]

Why not just use Any for summonFirst and then add the sound withFirst for sum types?
I needed the product variant for example to prove that at least one field is not empty to derive Reducible.
But I didn't really need to use the instance - it's just a proof.