I bought the book "Type Driven Development in Idris" and got several chapters in before getting distracted by whatever else. It was enough that I'm now annoyed relatively often that I can't pass types as parameters to be altered during execution. I really think they're onto something brilliant. I need to pick it back up and finish the book.
There are some minor changes, but they are documented in detail [1]. The Idris2 repository maintains tests to detect any further divergence from the book [2].
I highly recommend the book. Typing in examples and getting experience collaborating with the compiler on edits is worthwhile. Even if you never use Idris(2) again after reading it, the demos on creating state machine DSLs with contextual invariants will leave a lasting impression.
Well minor including the switch to use of so called “quantitative type theory” where you can include use counts for variables that inform the compiler how long variables will stick around. Also the compiler switch to Chez Scheme yields a pretty big performance boost.
You're right, there are several notable improvements in Idris2. I was mainly referring to the amount of code from the book that must be adapted. The QTT features, as you say, are opt-in; by default no new constraints are imposed.
Not really, Idris2 is very similar to Idris1 and the book is more on developing concepts/ideas rather than just being a cookbook of things to do in Idris1.
Dependent types let you do this. The type system ensures that you have all the types known at every point, and everything is sewn up before runtime - even though you don't know which type you will actually get ahead of time.
Types are values, and types can depend on values - so if your protocol tells you you should be getting a string, a string shows up in the type signature.
Types are not "altered". Types can be parameters. You can have a function that takes a type and returns something else (another type, or even another value). But nothing is changing.
As the workhorse example, consider the length-indexed Vector:
data Vec : Nat -> Type -> Type
Each Vec has its length in its type. You get a type error if you try the following:
f : Vec 3 Int -> Int
f [1, 2, 3, 4] -- error: wanted a Vec 3 Int, found a Vec 4 Int
and with that, consider the following program:
import Data.Vect
readInts : (n : Nat) -> IO (Vect n Int)
readInts 0 = pure []
readInts (S n) = do
x <- getLine
rest <- readInts n
pure $ (cast x) :: rest
main : IO ()
main = do
length <- getLine
ints <- readInts (fromInteger . cast $ length)
pure ()
The above program doesn't know what the type of `ints` is in the do-block precisely. It has a length specified by the user! But we can reason about its length - and the type system would ensure that its length is propagated and handled properly everywhere we try to use it.
It's just standard dependent types. Types don't (necessarily) get erased, but all the type checking itself is done at compile time.
I don't think it makes sense to think of it as specifically "statically kinded", since kinds (which are just types higher on the universe hierarchy) can also be present at runtime.
Indeed - the Type/Kind hierarchy is unified when you write a dependently typed system. In simply typed lambda calculus, you have a system of values, types, and kinds, which are required to make sense of the structure. In dependent types, you have values, and types, which are also values.
> Type/Kind hierarchy is unified when you write a dependently typed system
i'm being pedantic, but i don't think that's always the case. afaik
Type : Type
leads to "inconsistency" (sounds like Russell's paradox, but my knowledge of the theory gets flaky here). so e.g. in Coq there's actually a hierarchy of "universes":
> "[The type of Int is Set, ] the type of Set is Type(0), the type of Type(0) is Type(1), the type of Type(1) is Type(2), and so on."
The terminology is nearing its limit when talking about these kind of things.
I believe that static typing here means that there is no need for runtime dynamics type checks (outside of things like dynamic dispatch as with haskell typeclasses).
That is you can have a body of code where a variable can assume multiple incompatible types, but you always know that it will be the right one.
I would say it is a change in paradigm. Similarly to how rust' borrow checker and lifetimes change the paradigm of manual vs GC memory management
It is more that you can have values like `payload : if byte[TYPE_OFFSET] == TYPE_INT then Int else String`.
You are required to disambiguate the type before anything useful can be done. What has happened is that you have types being passed around by functions and evaluations which reflect dynamic behaviour at runtime - but there is a type statically known at all times for each part of the program.
