Skolemization de expressões de tipo existencial
No Scala, a seguinte expressão gera um erro de tipo:
val pair: (A => String, A) forSome { type A } = ( { a: Int => a.toString }, 19 )
pair._1(pair._2)
Como mencionado emSI-9899 e istoresponda, isso está correto de acordo com as especificações:
Eu acho que isso está funcionando conforme o SLS 6.1: "A regra de skolemization a seguir é aplicada universalmente para todas as expressões: se o tipo de uma expressão for do tipo existencial T, o tipo da expressão será assumido como skolemization de T. "
No entanto, eu não entendo isso completamente. Em que ponto essa regra é aplicada? Aplica-se na primeira linha (ou seja, o tipo depair
é diferente do indicado pela anotação de tipo) ou na segunda linha (mas aplicar a regra à segunda linha como um todo não levaria a um erro de tipo)?
Vamos supor que o SLS 6.1 se aplique à primeira linha. É supostoskolemize tipos existenciais. Podemos fazer da primeira linha um tipo inexistente, colocando o existencial dentro de um parâmetro de tipo:
case class Wrap[T](x:T)
val wrap = Wrap(( { a: Int => a.toString }, 19 ) : (A => String, A) forSome { type A })
wrap.x._1(wrap.x._2)
Funciona! (Sem erro de tipo.) Isso significa que o tipo existencial foi "perdido" quando definimospair
? Não:
val wrap2 = Wrap(pair)
wrap2.x._1(wrap2.x._2)
Este tipo verifica! Se tivesse sido a "falha" da atribuição apair
, isso não deve funcionar. Assim, a razão pela qual não funciona está na segunda linha. Se for esse o caso, qual é a diferença entre owrap
e apair
exemplo?
Para finalizar, aqui está mais um par de exemplos:
val Wrap((a2,b2)) = wrap
a2(b2)
val (a3,b3) = pair
a3(b3)
Ambos não funcionam, mas por analogia ao fato de quewrap.x._1(wrap.x._2)
fiz typecheck, eu teria pensado quea2(b2)
também pode verificar.