Idris examples taken from https://www.amazon.com/Gentle-Introduction-Dependent-Types-Idris-ebook/dp/B07H5M32YM/
The way this video went, you miss all the mean, unfair things I say about Idris.
The start of a new video series where I go through the book, Introduction to Programming in ATS, available at http://www.ats-lang.org/Documents.html#INT2PROGINATS
Use templates and functors to specialize code as needed.
Don't try to do everything with polymorphic functions.
I got a segfault while using a simple C library, why?
Trying something different--a screencast with typed instead of spoken commentary, against electro-swing. Music's compiled by Xefos Music @ https://www.youtube.com/watch?v=kfFfxJrKhLw
The coolest part of ATS!
Bob talking about TTD: https://8thlight.com/blog/uncle-bob/2014/04/30/When-tdd-does-not-work.html
More about this subject in section III of Introduction to Programming in ATS
Of course there would be 'runtime checking' in something like case+ x of knight(_) => ... | ninja(_) => ...; , as the tag value is what distinguishes a knight from a ninja.
@00:23, "just like an enum class in any other language".
The easy, we do immediately.
The ... still very easy, we also manage to do, in 46 minutes and 40 seconds.
@12:00, "Is there something wrong with the word default?"
yes. That's part of the switch syntax.
of getenv, rather than casting the return to ptr in order to test it, it could've been defined as returning ptr in the first place.
recorded: 25 May 2018
Created 2 months ago.
|Category||Science & Technology|
Subscribe to this channel for screencasts about the ATS programming language:
- ML derived
- Dependent types
- Linear types
- "Programming with Theorem Proving"
- As fast or faster than C (no joke)
- Viable with and without a GC
- Excellent FFI
Look for more at http://ats-lang.org/