Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Structural type refinement and type equality

I stumbled upon a puzzling behaviour of Type.=:= when applied on type refinments. Consider:

import reflect.runtime.universe._
type T1 = AnyRef {
  def apply( name: String ): Unit
  def foo: String
}

type Base = { def apply( name: String ): Unit }
type T2 = Base {
  def foo: String
}

Given that Base is an alias for a type refinement, I would expected that refining it further by adding the member foo would yield the same type as if I had defined foo right in Base.

Or in other words, I would expect that T1 and T2 denote entirely equivalent types.

For the most part, scalac seems to agree. By example I can pass an instance of T2 where an instance of T1 is expected:

def f( x: T1 ){}
f( null: T2 ) // scalac does not complain here

And conversely:

def g( x: T2 ){}
g( null: T1 ) // scalac is still happy

I can also ask for an evidence T1 =:= T2 and it compiles fine too:

implicitly[T1 =:= T2]

However, using scala reflection I get entirely different results:

scala> typeOf[T1] =:= typeOf[T2]
res2: Boolean = false

So is this a scala reflection bug (I would guess so) or is there a fundamental reason (technical of otherwise) why typeOf[T1] =:= typeOf[T2] would return false?

like image 349
Régis Jean-Gilles Avatar asked Feb 07 '14 13:02

Régis Jean-Gilles


People also ask

What is a refinement type?

In type theory, a refinement type is a type endowed with a predicate which is assumed to hold for any element of the refined type.

What are the different types of structural inequality?

Types of Structural Inequality. 1 1. Education. Students in low-income neighborhoods often receive an inferior education than students in wealthier areas. Research has found that this ... 2 2. Housing. 3 3. Health Care. 4 4. Race. 5 5. Gender. More items

What is a refinement type system in machine learning?

The type system "preserves the decidability of ML's type inference" whilst still "allowing more errors to be detected at compile-time". In more recent times, refinement type systems have been developed for languages such as Haskell, TypeScript and Scala .

Which programming languages have a refinement type system?

In more recent times, refinement type systems have been developed for languages such as Haskell, TypeScript and Scala . ^ a bFreeman, T.; Pfenning, F. (1991).


1 Answers

Sadly, it looks to be this bug: https://issues.scala-lang.org/browse/SI-8177

On the plus side... it looks like there's work actively underway to fix it :)

like image 125
Kevin Wright Avatar answered Oct 11 '22 20:10

Kevin Wright