How to fix this match type?

Question
1

How to fix the definition of Head in the code below so it compiles?

// Custom Tuple/HList type with upper bound
trait TList[+E]
case object Empty extends TList[Nothing]
case class Cons[+E, +H <: E, +T <: TList[E]](h: H, t: T) extends TList[E]

// Head function at the type level
type Head[E, L <: TList[E]] <: Option[E] = L match
  case Empty.type => None.type
  case Cons[E, h, ?] => Some[h]

The compile error, triggered by the last code line:

Found:    Some[h]
Required: Option[E]

where:    h is a type in type Head
1 Like
2

I guess you have to mimic the definition of Cons and add H <: E to Head?

3

But then I would need to know H in advance, which is what Head is trying to find out…

4

If Cons needs to know H in advance, it seems to me that Head would have to know it in advance too… doesn’t that make sense?

I’m not too strong in type theory but this seems to be going into existential types? Match types seem like they provide that feature but they don’t? (All the types we are matching need to be known?)

Aside: I noticed a few weird things, bugs maybe? If I change h from lowercase to uppercase H the error message changes… not found type: H makes more sense to me than the current message. where h is a type in Head means… what exactly? “in”?

Maybe consider using Idris or something… :smiley: Or you need alternate ways like path dependent types: add type members to your trait? I don’t know how to design that, not too familiar…

5

Does this work for you?

2 Likes
6

Yes, if we remove the bound on the return type it also works. But I thought this is probably not what Bersier wanted…

Aside: Here it says that variables in type patterns start with lowercase letters, so that resolves my earlier confusion.

Here is a different design with type members, what do people think?

2 Likes
7

@Bersier

Try

type Head[E, L <: TList[E]] <: Option[E] = L match
  case Empty.type => None.type
  case Cons[E, h, ?] => Some[h & E]
3 Likes
8

I am assuming that the type bounds will be guaranteed by construction. May be wrong though. But we have an answer now :slight_smile:

1 Like
9

Yep we do :smiley:
I’m not sure either.

Both the Option[?] and the Some[h & E] approaches satisfy the compiler, but I think the type member approach is the most accurate, in terms of the design intent (as far as I understand). h & E won’t be the same as h from compiler’s perspective; it’s a subtype of h.

Maybe the error in the original match type is a bug? :thinking: Looks like the compiler doesn’t know h <: E, or maybe it isn’t true and we need a way to tell the compiler. h is just what the docs call a “type pattern”, just a variable, so it does not have the <: E bound information from Cons ???

1 Like
10

Thank you all for replying!

@hmf I was aware of that solution, but didn’t find it satisfying, as the type bound is loose. It does look like type bounds only matter for recursive match types, however, so the type bound doesn’t have any impact beyond documentation in my example. So your solution does look like the simplest way to get Head to compile.

@spamegg1 The type member approach is interesting. It doesn’t scale to more complex functions, though, where the output doesn’t purely depend on the case. For Head however, it’s a nice alternative.

@DmytroMitin Intersecting h back with E is an ingenious solution! I had not considered that approach.

@spamegg1 I also wonder why the compiler doesn’t know that h <: E. And there doesn’t seem to be any way to add that constraint explicitly in the pattern either (for example with an @, as in term patterns).

@sjrd In case you have something to add.

1 Like
11

There are probably ways of doing it; but I’m not too familiar with path-dependent type design. The entire type system of Dotty is based on path dependent types, so I’m sure there is a way (but no resources to learn about it).

Could be a bug? Not sure. Hopefully someone more knowledgeable can tell us.