real

Interview with Albert

Albert

Hello Albert. You are one of the most active learners in my course «Introduction to programming with dependent types in Scala». Would you agree to give an interview to me?

Hi Dmytro,
I'd love to do the interview as I'm grateful for your kindly help on the type level programming lesson.
I've took quite a few MOOCs online, but none of the teachers spent so much effort on answering student's questions in such a timely manner. It feels like enjoying a private lesson, so as to speak I owe you a favour for this wonderful lesson.
It is perhaps some what related to the nature of this course, it is abstract and not easily followed. So right now not so many people are actively participating in it. Otherwise you'd be busy around all day long to answer all student's question.

Back to the lesson, I haven't felt I learned «type level programming». But now I know what «type level programming» is, what an automated proof is. It is fun to go through all lessons and fill in the blanks in the exercise. I might still have a lot to learn to truly understand and use it appropriately in my daily work.

I sincerely hope people like me who know a little functional programming and want to dig into this could enjoy this course as well.

Thank you for your warm words.
So let's start our interview.
Would you tell us several words about yourself?


Continue...Collapse )
real

Introduction to programming with dependent types in Scala

All videos are online. Totally 8 hours of video, 130 slides, and 50 programming exercises (in pure Scala and in Scala + ProvingGround library).
https://stepik.org/2294
1 Theory
1.1 Installing software https://goo.gl/ZmIdzy
1.2 Dependent types https://goo.gl/6AhLf7
1.3 Path-dependent types https://goo.gl/bWgUCr
1.4 Type classes https://goo.gl/zqx1ra
1.5 Product type https://goo.gl/KAdaSD
1.6 Co-product type (sum type) https://goo.gl/qogGSF
1.7 Function type https://goo.gl/j1fRio
1.8 Dependent pair type (Σ-type) https://goo.gl/h8cmDG
1.9 Dependent function type (Π-type) https://goo.gl/6hGcq3
1.10 Empty and unit types https://goo.gl/e9JTD7
1.11 Boolean type https://goo.gl/vlR833
1.12 Type of natural numbers https://goo.gl/lBnbh8
1.13 List type https://goo.gl/H64rOg
1.14 Type of fixed-length vectors https://goo.gl/9p5KwO
1.15 Identity type. Curry–Howard correspondence https://goo.gl/15EDMw
1.16 Eliminators into dependent types (induction) https://goo.gl/C2Mrd7
1.17 Type-level programming https://goo.gl/5XPk4K
2 Practice
real

Попиарим научный форум dxdy.ru


Буду благодарен, если попиарите форум среди знакомых.

Приглашаю посетить научный форум dxdy.ru. Более 100'000 сообщений, более 10'000 пользователей, около 15'000 тем по



Кроме высококвалифицированных участников форум от аналогов отличает давно и успешно реализованная возможность оформлять математические формулы в нотации \LaTeX. Например, в теме Проверка на простоту без такого наглядного и всемирно используемого инструмента просто не обойтись.

В общем, добро пожаловать! Помните, что за вас задачи у нас не решают, у нас помогут решить и разобраться, но основную работу должны проделать вы сами.


Если будете размещать у себя эту рекламку, то вот удобное окошко, чтобы скопипастить html-код:


Спасибо!

(c) cepesh