Interview with 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 )

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).
1 Theory
1.1 Installing software
1.2 Dependent types
1.3 Path-dependent types
1.4 Type classes
1.5 Product type
1.6 Co-product type (sum type)
1.7 Function type
1.8 Dependent pair type (Σ-type)
1.9 Dependent function type (Π-type)
1.10 Empty and unit types
1.11 Boolean type
1.12 Type of natural numbers
1.13 List type
1.14 Type of fixed-length vectors
1.15 Identity type. Curry–Howard correspondence
1.16 Eliminators into dependent types (induction)
1.17 Type-level programming
2 Practice

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

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

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

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

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

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


(c) cepesh