Zdravo Lambdoljupci!
Zadovoljstvo mi je predstavit novo Lambda druženje. Ovaj put igrat ćemo se sa Type-ovima i Kind-ovima. Otkrijte zašto ćete i vi zavoljeti dependent tipove ili ih možda potpuno zamrzit. Kako god bilo logika će sigurno biti dependently typed.
Da li ćete već za sljedeći projekt koristiti Idris? Nećete, ali utjecaj dependent tipova već i sad postoji u raznim jezicima.Za ovaj uvod izabrao sam primjere i demoe u Idris-u koji se reklamira kao general purpose jezik sa sintaksom vrlo sličnom Haskell-u. Bit će primjera i u C#/Java stilu, krećemo sa generics-ima. Obećavam i demonstraciju potpuno nerazumljivih grešaka (pravit ću se namjernih).
Prava snaga i ljepota ovakvih jezika je u mogućnosti da definiraju logički framework s kojim implementacija nove logike ne zahtjeva novi jezik već samo novi library. DSL sa univerzalnom domenom. 🙂
