Scala: how to create a type parametrized by a value, instead of a type

Is it possible to create, in Scala, a type which is parametrized by a value? Instead of defining a partial type List[A] and parametrize it with List[Int], I'd like to define a partial type (in pseudo-code) Element[Symbol] and parametrize it with Element['td]. In this example, the type represent an XML element: Element['td] informs th开发者_JAVA技巧e Scala type checker that we have a <td> element, and you can imagine that one could have APIs that specifically expect or return <td> elements.

(Subclassing, as inclass Td extends Element, is not a very satisfactory solution, as it doesn't prevent two pieces of code, maybe written by independent developers, from declaring different subclasses for <td>, which will then be considered to be different types by the Scala type checker.)

---

If you really want to parameterize a type by a value, you need a dependently typed programming language such as Agda.

---

Just some ideas to play with... Objects are values and they have a type.

trait XmlElement
object Td extends XmlElement

Then, you can have a parameterized class and use it on that specific type.

class Element[T <: XmlElement] { ... }
val elementOnTd = new Element[Td.type]
// elementOnTd can only be used with Td.

If there is only a fixed number of elements you want to support then you can make a sealed trait and your library will only work with those objects (though that seems pretty limiting)

sealed trait XmlElement
object Td extends XmlElement
object Tr extends XmlElement
// can't have anything other than `Td` and `Tr` !

The other thing you can play with is that inner classes of objects don't have the same type. So you can also do something along the line object Td { class Element { ... } } and Td.Element won't have the same type as Tr.Element.

---

It sounds like what you really want is not so much to parameterize a type by a value (like you could in C++) but to force various developers to agree on a common implementation.

I don't think that that is a problem the language would solve for you. Even if you force there to only be one way to have a <td> type, isn't there still discretion in what, exactly, that <td> type is?

If you really do want to parameterize a type by a value, you'll probably have to do something like:

object TD {
}

ie make it actually be a type, now you can write Element[TD]. Though that still has the problem that someone else could write object TD { } in another package and there'd be two of them.

You could try and emulate full dependent types using something like

object A { }
object B { }
object C { }
...

object TyString[Car,Cdr] { }

So that "TD" would be represented as

TyString[T,TyString[D,()]]

But you probably don't want to go there ;)

(I've heard that Scala was going to implement something called "singleton literals", but did that ever happen? You were supposed to be able to write "td".type, but Scala 2.9.1 doesn't accept that syntax).

---

Singleton types will give you want you're asking for,

scala> class Element[+T]
defined class Element

scala> val td = 'td
td: Symbol = 'td

scala> val p = 'p
p: Symbol = 'p

scala> def acceptAll[T](e : Element[T]) = e
acceptAll: [T](e: Element[T])Element[T]

scala> def acceptTd(e : Element[td.type]) = e
acceptTd: (e: Element[td.type])Element[td.type]

scala> acceptAll(new Element[p.type])       // OK
res3: Element[Symbol] = Element@628b54f4

scala> acceptAll(new Element[td.type])      // OK
res4: Element[Symbol] = Element@6e7eee36

scala> acceptTd(new Element[td.type])       // OK
res2: Element[td.type] = Element@547fa706

scala> acceptTd(new Element[p.type])        // Doesn't compile
<console>:12: error: type mismatch;
 found   : Element[p.type]
 required: Element[td.type]
              acceptTd(new Element[p.type])
                       ^

However, they're not giving you anything you couldn't already have had by creating a (sealed) family of types to represent element names. Note that there's nothing special about the use of Scala Symbols here: any stable identifier of a reference type gives rise to a unique singleton type which can be used in the same way.