bkil-syslogng
commented
7 years ago The language sounds interesting, with its C, Javascript and Java backends and functional roots, but I'd like to see how real applications would be developed with it, how it would look like a mixed environment, what kind if IDE support will be feasible in the near future, its performance, comparison to other bleeding edge and establish languages (Rust, Elixir, ....).
tamascsaba
speaker: Brian McKenna topic: Practical Dependent Types with Practical Examples video: https://www.youtube.com/watch?v=4i7KrG1Afbk length: 40:55
Dependent types turn types into a first-class language construct and allows types to be predicated upon values. Allowing types to be controlled by ordinary values allows us to prove many more properties about our programs and enables some interesting forms of metaprogramming. We can do interesting things like write a type-safe printf or verify algebraic laws of data structures - but while dependent types are quickly gaining in popularity, it can be tricky to find examples which are both useful and introductory. This talk will demonstrate some practical dependent typing examples (and not sized vectors) using Idris, a language designed for writing executable programs, rather than just proving theorems.
by Brian McKenna (@puf nfresh)
Brian McKenna is a small contributor to the Idris and PureScript languages. He also makes video tutorials on writing programs in Idris so that others can get started with dependent types. Brian works professionally as a functional programmer at a startup, using tools such as Scala and Haskell to create products for utility companies.