I'm a senior software engineer at Iterators, disguised under a self-proclaimed title of Scala Tiger (or Scala Kitten), sometimes also known as Scala Animal. I have been in this business for ca. 10 years, mostly filled with immense displeasure of working in C#, Java or Ruby until I witnessed the advent of FP in the industry and regained the knowledge I'd lost leaving academia halls. Embracing Scala helped me to become born-again programmer, type system theorist and category theory hobbyist. I gave talks at Krakow Scala User Group, Chamberconf, Scalapolis and ScalaWAW on subjects like: Kleisli arrows, category theory and Free monads. My coworkers wrote about me: "Don't let Marcin start talking about type systems... He is an expert using Scala to build most composable and concise business logic for our partners. " but I find it to be unfounded hype.
I will show how value-dependent types known from Idris can be used in Scala development by explaining how to express idiomatic Idris code in Scala. Audience will not only be able to learn a bit of the former language and its unique approach to type-safety, but also those with some Scala experience will see that VDT can be to a great extent simulated in the latter. Ultimately, I will try to elaborate on the question of if and how various forms of dependent typing are useful for a contemporary programmer.Slides