Get the top HN stories in your inbox every day.
satvikpendem
acchow
I had never heard of this book before, now I definitely want to give it a try.
As an aside, isn't type driven development how everyone codes naturally in statically typed languages? Whether it's Ocaml or Java, I feel like I try to get the types defined, then put on music and turn my brain off and just line the types up (much moreso in Ocaml than in Java).
henrydark
In my experience it's not at all how everyone codes, or even almost anyone, in statically typed languages. Here's an example to elucidate a (potential) difference between the common and the commitment to types:
You're coding a card game, say poker. Games should only start with a shuffled deck.
1. A reasonable, common solution would be to have a type like Deck, and a function shuffle, taking a Deck and returning a Deck (where taking can mean it's an instance's member function, and returning can mean inplace mutation)
2. A type driven approach can be having two distinct types: Deck and ShuffledDeck, and a function that takes a Deck and returns a ShuffledDeck, and all procedures henceforth in the game's logic require ShuffledDeck - _not_ Deck.
In the type driven approach the possibility of playing with an unshuffled deck has been removed solely through the usage of types, and successful compilation is a proof no cheaters can sneak in a bad deck.
But it's not just that. There's exactly one function that takes Deck and returns ShuffledDeck, so a language like idris knows this has to fill a hole somewhere, in the one place that starts with Deck and then need ShuffledDeck. So in some sense part of the code has been written automatically.
I rarely see the second approach used, though I see analogies of this example all the time.
bsaul
good example. i thought i used type-driven design, but your example made me realize i'm clearly not.
In your example, how would you qualify using an enum "State" with the case "shuffled" and "ordered" ? I feel like this would help me check all cases in places where it's needed, sometimes with the help of the compiler. But does that qualify as "type-driven" ?
In particular, do languages like idriss require encoding all possible states of a state machine as a unique type to leverage the full power of the checking mechanisms ? This would seem a bit unmanageable in practice..
yazzku
It's a bit more than that in Haskell (and I guess Idris, but never tried). In Haskell you can write 'undefined' in any definition. 'undefined' is of any type, so the code will type-check. Then you can write a high-level sketch of your program, including functions, purely based on types and 'undefined'. When you are satisfied playing the types puzzle, you proceed to write implementations. This is referred to as "hole-driven programming" or "type hole-driven programming".
Also, like the other guy mentioned, the types lend themselves very well to auto-completion. It's no coincidence than in Hoogle, you can often find a function by its type. E.g., what could "[a] -> [b] -> [(a,b)]" possibly do?
satvikpendem
Indeed, and this is precisely why I hate writing in dynamically typed languages like Ruby or Python; they hinder me from thinking about the shape of the program clearly.
Barrin92
this is putting the cart before the horse given that in any real-world facing application it's not the language that determines the shape of the program but the data and rest of the world that interfaces with your program.
Dynamic languages are in many ways simply a recognition of that fact, namely that data is sparse, incremental, changes and accretes and so on. There's a reason languages like Idris, Haskell and so forth are much more popular in solipsistic domains like theorem-proving than they are in a business application.
iddan
Well now you can write full types in both of them
undefined
grumpyprole
Don't forget that "type derived code" also happens with any language that has implicit arguments, e.g. type classes in Haskell and implicits in Scala. For example, in Haskell, if I compare two lists-of-maps-of-tuples for equality, there are many nested equality functions involved, but the type class machinery generates this code, at compile time for me. In a language without this, e.g. OCaml, many generic operations like equality, to_string, serialisation, etc become very painful.
still_grokking
Even "implicits" (especially the explicit ones called `given`s in Scala) are extremely useful I don't think you need them for type-class derivation. Rust does not use "implicits" for that, I think.
valenterry
How does Rust do it? Is it possible to derive using custom logic?
mcphage
> the logic itself can be produced automatically via the filling of type holes
Does that work in anything but boilerplate code? Like, hole filling won't be able to decide between then and else clauses in a conditional, for instance, because both clauses return the same type. And conditionals are one of the most basic data flow structures.
ekidd
> Does that work in anything but boilerplate code?
It depends on the problem and the language.
The most impressive I've ever seen was implementing "call with current continuation" as a monad, given nothing but the type signature.
Generally, it works best in strongly-typed, functional languages.
still_grokking
> The most impressive I've ever seen was implementing "call with current continuation" as a monad, given nothing but the type signature.
That sounds cool. Where to find this? I get only irrelevant search results.
ddejohn
To be honest, boilerplate is where I think I'd appreciate code generation the most.
mcphage
That makes sense, but it also seems like a “the cause of, and solution to, all of life’s problems” sort of situation.
josephcsible
For Boolean conditionals, you're right. But there are richer conditionals that make certain variables available in only one clause of them, e.g., matching on whether an Either in Haskell is Left or Right, or whether a Result in Rust is an Err or an Ok.
ddejohn
Today I learned that there's a name for the kind of development I do naturally. Modeling my input and output types first is so much more effective at helping me to develop my mental model of the program. I often catch "bugs" before I've started writing code just by thinking about how the data flow will work.
davidwritesbugs
The hopi is out of days though. It covers Idris 1 and isn't, I believe, being updated. Edwin intimated to me a while ago he'd rather have his bollocks cut off than write another book, and I assume he included updates in that. Idris 2 has significant differences to 1.
janjones
> the compiler can guess the implementation of the function [...] guaranteed to be correct on a type level
I'm curious about this. Can you provide some examples, please? Which languages can do this?
adamgordonbell
The guessing the implementation part is pretty cool. You can find videos of Edwin Brady showing it off on youtube:
https://www.youtube.com/watch?v=DRq2NgeFcO0
The book also walks you through lots of examples. The key part is the type needs to constrain the possible implementations down quite a bit.
jfoutz
off the top of my head, coq agda idris.
you can sort of do this with ghci and :hoogle.
the simplest example is
foo : A -> A
since we know absolutely NOTHING about A, all we can really do is give it back to you, so foo turns out to be identity, or id.
another might be bar: [A] -> Nat we still don't know anything about A, but we know a little about lists, so a good suggestion might be length.
All of the environments are pretty interactive, and you pick and choose. but from time to time there is exactly one possible implementation that meets all the constraints, so the compiler can fill that in.
dunham
Also "Wingman" for Haskell does some type-driven code generation. (It might be part of the haskell language server now, I get it when I use the vscode plugin.)
When the solution is ambiguous, Idris (and I believe wingman) will supply suggestions that you can pick from.
In your `bar` case, `bar xs = 42` is also a solution. Idris suggests 0 1 2 3 ... I think, it's going off of the constructors for the return type. I expect this technology to improve over time (try to use arguments, etc.)
Idris and Agda will also do stuff short of "fill in the answer" like "case split an argument for me" or "insert the appropriate constructor or lambda and leave a hole inside". This is quite helpful in cases where it's not gonna find the answer, but can type out the next step or two for you. (Wingman might have this, I haven't used it much. I don't know Coq at all.)
On the Agda side, the first couple of sections of "Programming Language Foundations in Agda" will walk you through using that functionality. Idris has a couple of videos that others have pointed out. It's fun stuff.
JadeNB
> foo : A -> A
> since we know absolutely NOTHING about A, all we can really do is give it back to you, so foo turns out to be identity, or id.
> another might be bar: [A] -> Nat we still don't know anything about A, but we know a little about lists, so a good suggestion might be length.
Certainly a good suggestion, but, unlike `foo`, not the only one—e.g., `bar xs = length xs + 1` or `bar xs = 2*(length xs)` also work.
Leherenn
While the concept is neat, I struggle a bit to see how it can be useful in practice. Do you have an example for the sufficiently constrained case? That sounds like the most interesting case by far.
undefined
p10r
Would you also recommend that book to someone who's not using Haskell/Idris/Scala?
satvikpendem
Sure, it's the methodology that's important, of making invalid states unrepresentable.
jshaqaw
I'm a big fan of this book for anyone interested in the topic: https://www.amazon.com/Gentle-Introduction-Dependent-Types-I...
gre
Better link... https://leanpub.com/gidti
CoastalCoder
Anyone know if there's a decent way to get a printed copy?
Or barring that, can anyone suggest a good device on which to read it and jot notes, for someone who normally prefers printed books?
nerdponx
I bought a basic b&w two-sided laser printer in 2011 for this purpose, and it's served me extremely well over the years. You can then take the stack of pages to a store like Staples and they will bind it for you for a few dollars.
I got the Brother HL-2270DW and I think they still make it. They even publish official Linux drivers for CUPS! Just make sure to get the extended toner cartridges (TN450), the regular ones are a ripoff.
kadoban
If you can find a used Remarkable 2 or something, that's a real nice experience. Great for textbooks and comics.
You can buy them new, but I think they've moved to some fairly insane forced subscription model.
Edit: looks like the forced subscription is no longer as bad as it once was
undefined
bor0
Hey, author here! Thank you for recommending my book. I am always happy when someone else finds my work useful :)
> Anyone know if there's a decent way to get a printed copy?
I decided to re-publish the book with Apress, and it should be ready for print by March this year.
> How is it better than tdd in Idris book?
I would not say it is better, or worse. I read TDD and it's a great book, but it was mostly focused on practical stuff (i.e. programming in Idris), and I found it lacking the theoretical explanations (for example, what proofs are and how to do a mathematical proof, or what is a type-checker and how to implement one) which I hoped to cover in my book.
jshaqaw
Adding onto the authors’s own review, I liked the second part on learning Idris but for my purposes the real gem was that it took me from zero prerequisites to a good intuition for dependent type theory in a very clear way that prepared me to go even deeper into topics like Homotopy Type Theory. The works I treasure are those that can build understandings of really complex topics without the crutch of a lot of prior assumed knowledge. It takes incredible clarity to do that well. This was one of my favorite book finds of recent years.
timmg
FWIW, I tried to read that book. It really didn't connect with me. Probably because I don't understand where it's going.
Does anyone have a good pointer to a different tutorial that tries to teach type-driven development?
rscho
Type Driven Development with Idris. You can find the link on the first answer of this thread. Among other things, the book shows an example of a state machine that cannot get stuck (by construction) to manage an ATM.
theusus
How is it better than tdd in Idris book?
jshaqaw
I can’t say. I’m just a hobbyist dilettante here. Maybe that other book is great too but I don’t know it. One fun thing about a language so deep down the rabbit hole as Idris is the mean caliber of people involved is higher than average.
peter_d_sherman
Looks highly interesting... Thanks for the suggestion!
pull_my_finger
Which version of Idris does this use?
peter_d_sherman
>"In Idris, types are first-class constructs in the langauge.
This means types can be passed as arguments to functions, and returned from functions just like any other value, such as numbers, strings, or lists.
This is a small but powerful idea, enabling:
o Relationships to be expressed between values; for example, that two lists have the same length.
o Assumptions to be made explicit and checked by the compiler. For example, if you assume that a list is non-empty, Idris can ensure this assumption always holds before the program is run.
o If desired, properties of program behaviour to be formally stated and proven."
PDS: I'd be curious to know about any/all languages where types can be passed to functions, returned from functions -- and even generated at runtime by functions... that is, where the language regards types as first-class constructs...
ihm
The most famous ones off the top of my head: Coq, Agda, Lean, Idris, ATS. Here's a list: https://en.wikipedia.org/wiki/Category:Dependently_typed_lan...
eggy
I tried ATS after finding Rust difficult. Zig is becoming my C replacement, and ATS is like a C++ replacement, although, I am using SPARK2014 now, but I am looking into ATS' contracts. There is no lack of PLs as a tool for whatever you may need to do nowadays. It's refreshing compared to 1970s to 1980s for me.
peter_d_sherman
That (and pages like that) are what I was looking for!
Thanks, much appreciated!
still_grokking
Scala is missing on that list (even it doesn't have "full dependent types" Match-Types are quite close).
csande17
Zig is probably the closest you'll get to this in an imperative language. You can write functions that take types as arguments and return types, and that's how e.g. generic data structures are implemented.
brabel
Terra is a language that can also do that, and uses Lua as the metaprogramming language. Types are just Lua values.
But unfortunately, there's a lot of work left kind of half-baked so using the language is a pain... if someone invested a lot of time to make Terra work properly and added some tooling around it, wrote proper docs and so on, it would be a really interesting language.
avgcorrection
> Terra is a language that can also do that, and uses Lua as the metaprogramming language. Types are just Lua values.
But then Terra doesn’t do that. Lua does. But not to itself, so it’s not really about passing around types as first-class values any more than metaprogramming Java in Python would elevate Java types to being first-class values.
still_grokking
That claim doesn't look correct.
Zig is just doing "compile time reflection". That's not even remotely close to dependent types.
The whole point of DT is that computed types can be used for type checking, and not only to compute values form them.
DT enable to reason about programs as mathematical proves. That's not possible in Zig, afaik.
If merely passing around values called "types" would be similar to what Idris does every language with runtime reflection and also all dynamic(!) languages would have DT. That's of course not true.
astrange
You can do that in Smalltalk descendants, if by types you mean metaclasses.
still_grokking
No, types are not runtime values!
That's the whole point.
That's why dependent types are so special (and complicated): You can use them as first class constructs without them being runtime values ever. Everything happens in the type checker.
At runtime there are no types in proper static languages; things like Java / C# are actually quite dynamic in contrast; the dynamic nature was even part of the marketing of those languages back than. (Runtime) reflection is just dynamic typing…
still_grokking
The examples are completely out of context.
> Relationships to be expressed between values; for example, that two lists have the same length.
This can be also expressed in any language, even in unityped (a.k.a. "dynamic") ones. You don't need types for that at all…
> Assumptions to be made explicit and checked by the compiler.
This can be also expressed in any language, even in unityped (a.k.a. "dynamic") ones. In theory you don't need types for that at all. (Even types would be the current std. method to achieve that).
> For example, if you assume that a list is non-empty, Idris can ensure this assumption always holds before the program is run.
You can construct a NEL (NonEmptyList) in any language. That's trivial. You just need to enforce the usage of the right factory method for your list.
> If desired, properties of program behaviour to be formally stated and proven.
This has nothing to do with dependent types (directly). A language based on simply typed lambda calculus is "enough" to arrive at this property.
dmytrish
Exactly, you can ship software in unityped languages. Still, how do you express even such a simple thing as a generic list type in simply typed lambda calculus?
It's just that dependent types enable you to express any invariants statically, without actually running the code.
> You can construct a NEL (NonEmptyList) in any language. That's trivial.
That's true, with the caveat of: this invariant only exists in your head and hopefully docs. When it's encoded in a type, your compiler gets awareness of this invariant as well. Then it's able to do things that were impossible before, it can catch bugs that you would not (e.g. due the sheer amount of source code).
Even though there are other approaches to software verification, types are the only one that got mainstream adoption so far.
still_grokking
Of course.
But the examples given missed the point imho.
All of the stated things don't need any type level machinery. You can just test things at runtime and be good.
If you want to prove things at compile time that's a very different story.
But than this needs to be explicitly stated in the examples.
cpurdy
>I'd be curious to know about any/all languages where types can be passed to functions, returned from functions -- and even generated at runtime by functions... that is, where the language regards types as first-class constructs...
Ecstasy (xtclang).
skybrian
Zig does some of this.
Functions can be written that can be called at compile time or runtime, depending on which language features they use.
Types can be computed and returned by functions in compile-time expressions.
I don't know how expressive the types can get, though?
Avshalom
I'm going to guess not very expressive. Zig refuses to have operator overloading because it might be used to call a function that's more expensive than you'd guess so the idea that they'd let types enforce all that much seems unlikely.
still_grokking
You can pass "types" also around in C#…
But in both cases that aren't types in the sens of type theory. In both cases those are just regular values (of type "Type"). In both cases you will be able to find those values with the help of a debugger. (The difference between Zig and C# being that in Zig those values are constructed during compilation and than mostly thrown away again whereas the "type" values are just regular runtime data on the CLR).
skybrian
The types created in compile-time code are just as "real" as the types you declare in source code.
All types become values at compile time. When you write a compiler, the parser creates ordinary values, perhaps instances of a Type type. The type-checking code operates on these values to find errors according to the rules of type theory. Compile-time functions are a way of calling user-defined code in the compiler, much like a macro but saner, and they can create types that can be used in declarations, verified by the type checker, and used as input to the code generator.
(Reflective use of runtime types in languages like C#, Java, or Go is different.)
kitd
This is presumably not what you're thinking of but ofc Javascript uses objects as prototype "types". As is, they wont provide what you want, but if there was some kind of "compile-time" processing of prototypes such that types assemblies, dependencies, constraints and other relationships could be manipulated or asserted before they were applied in runtime code, that may provide some of the "first-class type" functionality mentioned.
Ed: actually, Typescript might be a better host for this.
still_grokking
The down-votes are likely because the example isn't anyhow good.
But the idea to have static prototype types is imho quite interesting on its own. I was thinking a lot about that in the past.
I would love to have JS like objects—but in a static context.
Row polymorphism and extensible records are close but still not there actually.
eckza
FP Or Die Gang is downvoting you, but this is actually correct.
No referential transparency (among other things, no doubt) makes this a harder problem to solve than just using a language that supports it.
$0.02
still_grokking
If you don't have referential transparency mathematical equations don't hold. You can't be sure that `a = b` stays true if deducted once.
So "the problem" doesn't get only harder, it becomes impossible to solve in a formal way.
teddyh
> PDS: I'd be curious to know about any/all languages where types can be passed to functions, returned from functions -- and even generated at runtime by functions... that is, where the language regards types as first-class constructs...
Python does this.
still_grokking
Python is a dynamic language so it's completely out of competition here.
Types in the context of dependent types mean solely static types.
Runtime "types" are not types at all. They're runtime values.
undefined
peter_d_sherman
There also seems to be some intersection here between type-driven development and Proof Assistants:
chills
peter_d_sherman
Wowzer!
That is quite the page...
There is definitely something there!
That page is decidedly worth reading and re-reading many times in the future...
I think it boils down to the following:
>"Curry–Howard correspondence [...] is the direct relationship between computer programs and mathematical proofs."
And:
>"If one abstracts on the peculiarities of either formalism, the following generalization arises: a proof is a program, and the formula it proves is the type for the program."
In fact, I'm going to go for "full crackpot" here...
If all computer programs are algorithms, and all mathematical proofs are algorithms, and all types are algorithms -- then a "grand unifying theory" between Computer Programs and Mathematics -- looks like this:
It's all Algorithms.
Algorithms on top of algorithms.
You know, like turtles on top of turtles...
This makes sense too, if we think about it...
Algorithms are just series of steps, with given inputs and given outputs.
That is no different than Computer Programs.
And that is no different than Math...
You can call this series of steps an Algorithm, you can call it a Function, you can call it y=f(x), you can call it a Type, you can call it a Computer Program, you can call it a Math Equation, you can call it a logical proposition, and you can use whatever notation and nomenclature you like -- but in the end, in the end, it all boils down to an Algorithm...
A series of steps...
Now, perhaps that series of steps -- uses other series of steps -- perhaps that Algorithm uses other Algorithms, perhaps that function uses other functions, perhaps that Computer Program uses other computer programs, perhaps that Math Equation uses other math equations, etc., etc. --
But in the end, in the end...
It's all a series of rigorously defined steps...
It's all an Algorithm...
Or Algorithm consisting of other Algorithms... (recursively...)
Patterns of steps -- inside of patterns of other steps (again, recursively...)
Anyway, great page, definitely worth reading and re-reading!
schoen
If you're excited about that, you might enjoy
https://softwarefoundations.cis.upenn.edu/
Officially you're supposed to download the book and then edit the exercise solutions into it with Emacs (or VSCode, I think), as you can then run the exercises to see if they type-check (i.e., if they're correct!). However, there's also a not-necessarily-up-to-date interactive in-browser version:
https://jscoq.github.io/ext/sf/
I haven't used Idris, so I'd say it's quite possible that working through the Idris book is also just as fun and relevant for understanding the implications of the Curry-Howard correspondence.
consilient
> all mathematical proofs are algorithms
They're not. Only constructive proofs have corresponding programs (namely, the program that actually carries out the relevant construction). You can embed nonconstructive proofs indirectly via double-negation translation (computational counterpart: continuation-passing style), but equivalence of classical formulas isn't preserved.
> all types are algorithms
Definitely not the case. Types correspond to propositions, not their proofs.
rbonvall
I think you will enjoy this talk: https://www.youtube.com/watch?v=IOiZatlZtGU
still_grokking
I think you're missed the elephant in the room.
"Programs as proves" is only a thing in the context of mathematically pure languages.
Almost all programming languages aren't pure.
That's on the other hand's side why prove assistants are very unusable as programming languages; you can't do anything with them usually besides proving stuff. Running actually "useful" code is mostly not possible. Things like Haskell or Idris try to bridge both worlds, but this isn't straight forward. How to actually do anything in a pure programing language is still an open question. Monads are some kludge but not very practicable for most people…
So to summarize: "Normal" programs don't correspond to proves in any way!
jshaqaw
A huge overlap. Idris is aimed at being a general purpose language with proof assistant characteristics while some of its peers are more theorem provers built with general purpose language characteristics.
spelunker
Here's an intro to dependent types from David Christiansen, I think it came up during another dependent types discussion: https://youtu.be/VxINoKFm-S4
theresistor
What's the state of Idris2 at this point? I really enjoyed Type Driven Development with Idris a few years ago.
still_grokking
It's the current version.
https://www.idris-lang.org/idris-2-version-060-released.html
Idris 1 seems obsolete since years. No news about it for a long time.
ykonstant
I am dabbling in the cousin language Lean right now, and it is very fun to use!
peter_d_sherman
Some quick info for Lean:
Homepage: https://leanprover.github.io/
Source: https://github.com/leanprover/lean4
Wikipedia: https://en.wikipedia.org/wiki/Lean_(proof_assistant)
agentultra
I also wrote a guide: https://agentultra.github.io/lean-4-hackers/
still_grokking
LEAN's syntax looks really great. I wish Scala could take some inspiration.
Scala's syntax is anyway quite similar already, but would need proper Unicode support and some other "tuning" like the `:=` and the `let monadic ← effect` syntax, imho.
daxfohl
One difference I see is Lean uses type classes while Idris uses implicits. Can anyone comment on the pros and cons of that decision? (Or pros and cons between the two languages in general?)
It also seems that Idris was created as a general-purpose language first, whereas Lean started as a proof assistant and only recently added general-purpose language. Is that evident when using the languages? A quick look at Lean's general-purpose language seems reasonably similar to the Indris experience AFAICT.
ImprobableTruth
Imo the biggest difference is the "heritage", Lean is Coq inspired, Idris Agda inspired. This manifests in how people prove things. Idris has dependent pattern matching, so proofs are written as normal terms. Lean has tactics and proofs are small tactics scripts (which then generate the proof term behind the scene).
Other than that, the difference is mainly in infrastructure/libraries and community.
lapinot
Well, idris (v2) is very special since it has modalities for compile-time erasure and linearity. This sets it apart from all the other dependently-typed languages. This makes it possible in theory (and currently being experimented with) to implement efficient-by-construction code.
undefined
julianeon
Speaking of cousin languages, it looks so much like Haskell.
sunshinerag
Idris 1 was written in Haskell I think
mcdonje
I know I'm missing something, but this seems like the functional version of object classes.
I've mostly favored procedural programming and only use objects when I have to because the abstraction can make the program harder to reason about, especially when there's a lot of inheritance.
But I've heard some hype about types in Rust, and now this. The free chapter in the manning book even introduces types in terms of real world objects.
So, for someone who doesn't love objects, why should I love types?
ImprobableTruth
IMO types are fundamentally about restriction. Limiting the shape of your data and what you can do with it, so that this information becomes explicit - making it easier to reason about the program, both for yourself and the compiler. I think this is illuminated very well by sum types. If you have a variable of X | Y, you know that it's either exactly X or Y. You can pattern match, to handle the case that it's an X and then you call a function on it and you know exactly which function it is.
Inheritance is so nightmarish to me because people tend to use it in such a way that I often don't have the slightest clue what I'm actually dealing with, buried under layers of indirection that seem to serve absolutely no purpose. If I have an object of class X, is that actually an X, or something that just looks like it and actually behaves differently because someone decided to override a method in a subclass?
Interfaces tend to be much less monstrous IME, so I don't think the issue is with abstractions themselves. Especially when people use interfaces to abstract over common behavior between data types, rather than trying to future proof for something that never occurs.
still_grokking
I don't know of any sane language that does not support interfaces.
Type-classes are also just interfaces.
Additionally quite some orthogonal concepts are mixed up here: Classes, inheritance, overriding, runtime types, patterns…
In the end OO and FP are anyway the same thing at the core. You can mechanically translate one into the other:
ImprobableTruth
...C. I thought the context here made it obvious, the person I replied to was talking about programming in a procedural manner and eschewing abstractions.
I never even mentioned anything that even relates to runtime types, I don't know why you'd bring them up?
And saying that classes, inheritance and overriding are orthogonal is bizarre. They're intricately linked and at the heart of OOP. It doesn't even make sense to define overriding without inheritance.
>In the end OO and FP are anyway the same thing at the core. You can mechanically translate one into the other:
Coinductive types have destructors so they look a bit OO-ish, but that's it. The key part of OO isn't having fields, but inheritance.
josephcsible
> I've mostly favored procedural programming and only use objects when I have to because the abstraction can make the program harder to reason about, especially when there's a lot of inheritance.
In functional programming, you generally abstract in different directions than you do in object-oriented programming. IMO, functional abstractions make things easier to reason about, since they generally constrain what any given block of code might do.
> So, for someone who doesn't love objects, why should I love types?
Because powerful type systems mean that a lot of mistakes will be compiler errors instead of bugs.
ok_dad
Where objects can hide state or I/O in a program, types and functional type driven development make each function very clear as to what it has for input and outputs and part of that is not hiding state anywhere that doesn’t make sense. You might still have a global logger because that makes sense, but generally you know the things you have access to because they’re in the function signature.
It can break down if you aren’t careful, and there’s some nuance where you might still store a configuration data as an object property, but it’s a clearly typed property that’s assigned at initialization rather than hidden state that magically appears due to some hidden program flow.
still_grokking
Objects and types are quite different concepts.
Objects are just "things" in the memory of a computer. Anything in a program is an object. That's why for example the C guys are constantly talking about objects, even C does not have any special facilities to handle more complex types of objects.
Types on the other hands side are an abstract concept. You could think of them like sets of objects (even this is a little bit misleading as types are not really sets, but types, which is a different, but in some ways quite similar, mathematical concept).
What looks quite similar are types and classes. In OOP languages both are bound to each other: A class describes a set of objects (as a class is a kind of template for objects) and it introduces at the same time a corresponding type (which is as mentioned also "a set" of objects).
The interesting thing about types is, as they're an abstract concept, they exist independent of running your program. (Objects OTOH manifest not before they get constructed at runtime in the memory of a computer). With the help of a sound type system it's possible to prove things about the runtime behavior of a program. That's where the value of types comes form. They allow to construct more correct programs by ruling out errors by type-checking a program, which can be done in the case of a static type system at compile time.
Stronger type-systems allow to constrain the possible runtime behaviors of a program better and more precisely. They help to make illegal program states unrepresentable.
Also it gets possible to deduct correct-by-construction implementations of some program behaviors solely form types. That's what type-driven development is about.
So, if you don't like runtime bugs but correct programs you should like strong static typing.
allochthon
I recently watched this intro to the topic, which I found really interesting: https://www.youtube.com/watch?v=bnnacleqg6k
mcdonje
That was a good talk. Thanks for linking it.
jshaqaw
A can’t miss awesome thing for people on the precipice of the dependent type theory rabbit hole is 1lab: https://1lab.dev/#lab
1lab is the future for mathematics research that deserves to happen.
still_grokking
It's a pity I can't up-vote more than once.
Really great resource! Thanks for sharing!
truth_seeker
Recently I came across this fascinating live coding talk on Rust which focus on traits and structs to build extensible software APIs
Type Driven API - https://www.youtube.com/watch?v=bnnacleqg6k
Type level programming - https://willcrichton.net/notes/type-level-programming/
wellanyway
...because Haskell isn't ivory enough anymore.
nightowl_games
Anyone else finding this documentation is pretty hard to navigate? Makes me think this isn't a serious language, but rather an academic toy or resume builder.
andrewmcwatters
The main repository is in the top 1% of stargazed repositories on GitHub, and the project has a mailing list, Discord server, IRC, AND Slack.
It has been forked over 300 times, and has over 100 contributors.
What in the world counts as "serious" to some of you people?
Sometimes I read HN and ask myself if people here know at all how hard it is make something people want, and how many people know what the real-world thresholds are for understanding when you have made something that people want.
I guess if everyone hasn't heard of it, people here don't think it's serious.
mejutoco
I find Idris incredibly interesting. Specially combined with the output it can generate in other languages. The book of it is also a masterpiece, even if you never program in it. Already lots of "serious" hacked together programming languages.
The only downside I see if the lack of a package manager.
Kranar
>What in the world counts as "serious" to some of you people?
For a programming language? Would be good to know what projects have used it. Most languages people develop are done as either a hobby or to serve some kind of research/academic purpose. Is Idris used for any production grade software?
bobleeswagger
[flagged]
andrewmcwatters
I mean you tell me, which would be bullying to you? You work for years on something and someone tells you it's not "serious" because they haven't learned to browse a source tree, or the guy telling him to read a little more?
Either way, I apologize for how it came off.
wk_end
TBH I actually think the documentation for Idris is quite good, but your overall point is correct: it's definitely somewhere between "academic toy" and "serious language". It's not really usable for anything real world at the moment, and - like I comment every time it pops up here - just as it was building up momentum the author scrapped the whole thing and started over (Idris 2), and even though I've been making that comment for years it still hasn't recovered. The book everyone recommends to read on it is based around a dead version of the language; the tooling it has you use (which is a huge part of working with a dependently-typed language) depends on Atom, which is now dead, and Idris 2 still doesn't have comparable IDE support.
I find it really frustrating because I like the language a lot, and I want to be using dependent types in my real life ASAP. Right now I'd be looking more towards Lean, though, which seems to be more modern and developing rapidly.
hjadal
The Atom implementation has been replicated in VSCode and works alright. It was good enough for me to learn how Idris worked and go through the book's exercises.
CoastalCoder
> Anyone else finding this documentation is pretty hard to navigate?
I can't speak to these docs in particular, but I think documentation regarding type-system in general can be hard to digest. And it probably varies by reader.
E.g., some people find "The Little Typer" [0] to be a wonderful intro to its topic. Personally, I find the writing style impenetrable.
> Makes me think this isn't a serious language, but rather an academic toy or resume builder.
If the documentation turns out to be useless to the majority of readers, then you might be right that it's a sign of under-investment. I'm not sure if that's happening here.
There was a good interview on Corecursive [1] about Idris, so IMHO that's some evidence that some people are serious about the language.
[0] https://mitpress.mit.edu/9780262536431/the-little-typer/
[1] https://corecursive.com/006-type-driven-development-and-idri...
revskill
I think it's the chicken-egg issue. Firstly it's not the tools'fault. But overall, the culture of using that tool made it worse.
For example, most of readthedocs documentation i've seen is nothing better a wiki page, where you have a bunch of links to click on in a messy way somehow.
So i guess your issue with this one, is you're missing some structured knowledge with this page.
Get the top HN stories in your inbox every day.
The book itself Type Driven Development with Idris is great too, it is the principal way I write code these days, by writing my types upfront then filling out the logic, and in some languages, the logic itself can be produced automatically via the filling of type holes. In other words, simply based on the types you provide, the compiler can guess the implementation of the function, somewhat like Copilot but guaranteed to be correct on a type level, even if not necessarily on a business logic level.
https://www.manning.com/books/type-driven-development-with-i...