Talk in Italian at NoSlidesConf 2017
Track Name:
Agua Verde hall
Short URL: https://joind.in/talk/2aa2b
(QR-Code (opens in new window))
Types are a precious instrument to document our code and to catch errors at compile time, but they could be much more.
What if we could use types to drive our design process, to model precisely our domain and continuously receive feedback on it while we produce code? What if we could not only use types to find errors but also to actually prove the absence of errors?
If we introduce types as a first-class language construct, all of this, and much more, becomes possible.
In this talk we will see how to bring into play the full power of types using Idris, a purely functional programming language with dependent types, letting the types guide the development and being assisted by the compiler itself.
Comments
Comments are closed.
I know the talk was about the type system but, giving the language is not so popular, a brief introduction on it would have helped.
The talk fulfilled the title and shows how the language can shape a type only to accept well formed data but maybe the example is a bit too detailed.
As far as I understood, In the ending part of the talk it's shown how the hanoi tower can be implemented in a command line application where all the work done to make the input be acceptable to the data structure is kind of repeated (in logic) to do the acceptance of the input in the UI. I see this as a repetition and I've like to have some treatment of this subject: bad and good practices on what is necessary to shape in the type system and what in the business logic.
Thanks Gian Carlo for your feedback.
In general I prepared the talk trying to find the best way to pass the ideas and the techniques that Idris allows you to use, without focusing too much on the implementation details.
I hoped that the syntax, being not that far from the one used in many other functional languages, would not stop people from getting a glimpse of the possibilities of the language.
Maybe I could have skept some implementation details and tried to spend a bit more time on the ideas.
Regarding your last point, I don't think there is any repetition; in the domain you ask for something that needs to be provided in the outer application layer. If you want to check the whole solution, with the IO handling, you can check the whole code here: https://github.com/marcosh/idris-hanoi. Moreover, I would have loved to show also the effect handling part, since Idris handles it nicely, but it was really not possible to fit it all in 45 minutes.