Alexander Kuklev (akuklev) wrote,
Alexander Kuklev

SIP: Dependent type syntax for Scala

The key feature of dependent type systems is that we can write type-valued functions. Recently I encountered a case I could use such one in Scala for improving code readibility. I want to be able to write Reads(res1, res2) to get (ReadsAbstract {val reads = Set(res1, res2)}. Well, there are no type-valued methods in Scala, but I'm still able to get really close to it:

def ReadsGenerator(res: Resource*) = {

  new {type X = ReadsAbstract {val reads = Set(res:_*)}}


Now we can write Reads(res1, res2).X for the purpose I originaly wanted to use Reads(res1, res2) for.

It's worth to define some syntactic sugar for it! First, down with that nasty X. Second, let's add some sugar for generators:

type Reads(res: Resource*) = ReadsAbstract {val reads = Set(res:_*)}


– Such syntax can be easily extended for support of macro types in exactly parallel fashion to current syntax for macro methods. Like type DbTable(jdbcPath: String, creds: DbCredentials) = macro impl

– With this syntax we also obtain nice syntax for dependent tuples and dependent function types.

I would like to thank Nada Amin (ندى أمين) from EPFL for a very insightful discussion on DOT, the future of the Scala type system.
Tags: scala

  • О программировании, из комментов у vit_r

    orleans: У ФП есть обьективные преимущества в плане исполнения на многопроцессорных системах и организации юнит тестов. Все то что можно…

  • Effect typing in short

    There are many different classes of functions out there. There are pure functions and there are functions with diverse side effects. Some can perform…

  • Towards Scala 3

    I'd like to share some ideas on features that might be included into next major Scala releases. Some of them might come in question already for Scala…

  • Post a new comment


    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.