Also, with strong type systems (that encode behavior checks) how do I go about writing code incrementally and evolving the design as I go?
-
-
Replying to @waterlink000
Most strong type systems have special constructs that unify with everything. E.g., unimplemented!() in Rust. Also, sometimes, languages allow you to forward errors to Runtime. It’s not as good as dynamic languages, but there’s ways.
1 reply 0 retweets 0 likes -
Replying to @Argorak @waterlink000
It’s a hidden gem of Idris that it’s actually built around incomplete programs in development, a thing
@edwinbrady has given some good talks about.1 reply 0 retweets 0 likes -
Replying to @Argorak @waterlink000
Indeed. Types can evolve as well as programs. I generally refine the types as my understanding of a problem develops.
1 reply 0 retweets 0 likes -
Replying to @edwinbrady @Argorak
@edwinbrady could you share a link to a post or a video, where there is a small example of parallel evolution of types and the implementation, so that I can understand how it looks in practice better?1 reply 0 retweets 0 likes -
Replying to @waterlink000 @edwinbrady
I've seen this one: http://events.techcast.com/bigtechday9/barcelona-0900/?q=barcelona-0900 …
2 replies 0 retweets 0 likes -
Replying to @Argorak @waterlink000
I don't know if I have anything nice and concise that talks about this specific idea though. There's a few in passing in http://tinyurl.com/typedd but I suppose this might be a good topic for another talk some time...
1 reply 0 retweets 0 likes -
Replying to @edwinbrady @waterlink000
Well, it sold me quite good on it while I was actually just waiting for Alex Crichton speaking after :). But yeah, it's an hour and I don't think it's ready-made examples. Need to rewatch.
1 reply 0 retweets 0 likes -
Replying to @Argorak @edwinbrady
I’m watching the talk right now (~20min), and it got me thinking: TypeDD doesn’t seem to force me to decouple my code. That is one of the reasons I use TDD — it forces me to do that, and only to an extent needed (kind of like a sweet balanced spot).
1 reply 0 retweets 0 likes -
Somewhere around ~30min I’ve come to the realization that the “append” example is not exhaustively verified by the type: Only the lengths have to be right. If my algorithm screws up the order or does something else to values, this type definition is not concerned with that.
2 replies 0 retweets 0 likes
Yes. Types aren't there to show everything. Types and tests are completely compatible! You can, and should, write tests too.
-
-
Replying to @edwinbrady @Argorak
I agree, totally. There are definitely folks who are looking at dependent types with shining eyes and telling to themselves that it is their salvation from tests (I know at least one friend of mine, and there are few folks around on Twitter). That misunderstanding is bothering.
0 replies 0 retweets 0 likesThanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.