Search code examples
scalatypespath-dependent-typedependent-type

How to emulate a dependent type in Scala


I'm trying to define a generic residue class ring in Scala. A residue class ring is defined by some base ring (e.g. the integers) and a modulus (e.g. two), which is a value from the base ring. Both rings and their elements are objects, hence the type of the modulus would normally be a dependent type, depending on the base ring. I understand this isn't allowed in Scala (for good reasons), so I'm trying to emulate it by approximating the type and doing a runtime check when the residue class ring is constructed.

The definition of ResidueClassRing is accepted without error, however, Scala doesn't let me instantiate it, for the argument two I get the error message

type mismatch;
found   : dependenttypetest.DependentTypeTest.two.type 
(with underlying type dependenttypetest.Integers.Integer)  
required: dependenttypetest.EuclideanRing#E

Am I doing something wrong? Could this be a bug in the Scala type checker? Is there a better way to define ResidueClassRing?

This is with Scala 2.8.0 in the Eclipse IDE for Helios. The problem already occurred for 2.7.x. Here is a simplified version of the code:

package dependenttypetest


class EuclideanRing
{
  thisRing =>

  type E <: EuclideanRingElement;

  def one: E;

  trait EuclideanRingElement 
  {
    def ring = thisRing;

    def +(b: E): E;
    def %(b: E): E;
  }
}


object Integers extends EuclideanRing
{
  type E = Integer;

  val one: Integer = new Integer(1);

  class Integer(n: Int) extends EuclideanRingElement
  {
    val intValue: Int = n;
    def +(b: Integer): Integer = new Integer(intValue + b.intValue);
    def %(b: Integer): Integer = new Integer(intValue % b.intValue);
  }
}


class ResidueClassRing (val baseRing : EuclideanRing, m : EuclideanRing#E) 
{
  val modulus: baseRing.E = 
    m match {
    case e: baseRing.E if m.ring == baseRing => e;
    case _ => throw new IllegalArgumentException("modulus not from base ring");
    };

  type E = ResidueClassRingElement;

  def one: E = new ResidueClassRingElement(baseRing.one);

  class ResidueClassRingElement (e : baseRing.E)
  {
    def representative: baseRing.E = e % modulus;

    def +(b: E) = new ResidueClassRingElement(
      this.representative + b.representative); 
  }
}


object DependentTypeTest extends Application
{
  val two = new Integers.Integer(2);
  val mod2ring = new ResidueClassRing(Integers, two);

  println(mod2ring.one + mod2ring.one);
}

Solution

  • This seems to work, but I couldn't get rid of the cast when calculating representative:

    package dependenttypetest
    
    abstract class EuclideanRing{
      thisRing =>
      type E <: EuclideanRingElement;
      def one: E;
      trait EuclideanRingElement
      {
        def ring = thisRing;
    
        def +(b: E): E;
        def %(b: E): E;
      }
    }
    
    class Integers extends EuclideanRing {
      type E = Integer;
      val one: Integer = new Integer(1);
      class Integer(n: Int) extends EuclideanRingElement
      {
        val intValue: Int = n;
        def +(b: Integer): Integer = new Integer(intValue + b.intValue);
        def %(b: Integer): Integer = new Integer(intValue % b.intValue);
        override def toString = "Int" + intValue
      }
    }
    
    object Integers extends Integers 
    
    class ResidueClassRing[ER <: EuclideanRing] (modulus : ER#E) {
      val baseRing = modulus.ring
      type E = ResidueClassRingElement;
      def one: E = new ResidueClassRingElement(baseRing.one);
    
      class ResidueClassRingElement (e : baseRing.E)
      {
        def representative = e % modulus.asInstanceOf[baseRing.E];
        def +(b: E) = new ResidueClassRingElement(
          this.representative + b.representative);
        override def toString = "RC(" + representative + ")"
      }
    }
    
    object DependentTypeTest extends Application {
      val two =  new Integers.Integer(2);
      val mod2ring = new ResidueClassRing[Integers](two)
    
      println(mod2ring.one + mod2ring.one)
    }
    

    BTW: Be careful with the Application trait, it's rightfully deprecated.