Does the dependent types of Dotty allow for the same abilities Idris provides?

Question
1

Hi,

I like the Dependent Types of Idris, I’m curious to know if Dotty is able or could be able to provide the same abilities that programming in Idris gives.

Philip

2

I’m not into Idris, but from what I read I assume that Scala dependent typing is limited to types depending on terms using what is called “path-dependent types”.

In practice you can define types as part of objects, such that each object instance will carry his own specific value of the declared type.

How this compares with Idris DT is out of my expertise

3

Idris allows types to depend on terms, with arbitrary computations done at
compile time. The scala compiler, and I assume the dotty compiler, will
only recognize path dependent types as equal if they are from referential
equal objects, not from those that are equal by the == method. For
instance, in the ammonite REPL

@ class WithInner{class Inner; val inner = new Inner}
defined class WithInner
@ case class Named(name: String) extends WithInner
defined class Named
@ val me = Named("me")
me: Named = Named("me")
@ me.inner == me.inner
res6: Boolean = true
@ val meToo = Named("me") // equal to me
meToo: Named = Named("me")
@ meToo.inner == me.inner
res9: Boolean = false

Implicits are computed at compile time, and a lot can be encoded in this.

regards,
Siddhartha

4

Hi,

Yes so one problem with this question is you need to be familiar with both Dotty’s dependent types and Idris’s dependent types, since I am not completely familiar with both I can’t work it out and I guess not too many people are familiar with both.
I am “wildly guessing”!! perhaps Scala’s Macros combined with Path dependent types can do at compile time what Idris can do?

Philip