16 ms·

Types

445 points by ivank 10y ago

th0ma5 10y ago
Hope this makes it into Wikipedia instead of here.
- paulddraper 10y ago
  It'll get moderated out.
  - NhanH 10y ago
    For this article specifically, it shouldn't be on wiki. The quality still needs a lot of polish, and too much opinions.
    - gary_bernhardt 10y ago
      This is a decent summary of why I'm doing it. Wikipedia is full of "high quality" content, where "high quality" means "directly exposing every detail that anyone ever thought to nitpick", and this topic is a nitpicker's paradise. There's value in that detail-heavy style, but it's difficult to learn from and it's a type of writing that I rarely want to read. As for opinions (and lack thereof), they prevent Wikipedia from saying many things that are both well-known and easily stated. The lack of clear summaries of widespread disagreeing opinions keeps our implicit knowledge implicit.
      - NhanH 10y ago
        I agree with your reasoning and your description of Wikipedia. However, despite all the flaws, wiki is reasonably helpful, and I doubt filling it with more opinions would be helping the case.
twblalock 10y ago
The Idris example seems to need further explanation: > In Idris, we can say "the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument": > add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat > add x y = x + y That's all well and good, if you know the values of x and y at compile time. Consider a program that reads x and y from STDIN. The user could provide an x that is equal to or larger than y (or could provide only one value, or values that are not numbers). I see no way to deal with that except to throw a runtime error. Is that what would happen?
- platz 10y ago
  not in idris, because it would force you to do that check manually and pass in the evidence as proof. it has a bunch of tools to help you do this.. namely lifting values into types with 'dependent pairs'. idris doesnt automagically calculate everything for you, but makes sure at compile time, that you provide evidence at run time for the things you have asserted in the types. it makes more sense after going through some of the tutorials and books.
- NhanH 10y ago
  I do NOT know anything about Idris, but I'd imagine you have to do a check along the line of `if (x<y) then` before being able to call `add`, within that block-scope, the compiler should be able to infer that x<y. Typescript has something similar, where if you do `if (foo)`, the compiler will know that foo can't be null or undefined.
- _ibu9 10y ago
  The missing explanation is that `smaller` is a third argument to the function. It's type is a proof that x <= y. Since it is in curly brackets with the auto keyword, the compiler will fill in this proof in many cases, like when the values are statically known. In the case where the values are read from the external environment, first you would have to compare them before calling the function. The comparator would return either a proof that x <= y, or x > y. In the first case you plug that value into the `smaller` argument, in the second case it's your responsibility to signal whatever kind of application-specific error is appropriate (assuming x > y is some kind of erroneous condition).
lqdc13 10y ago
I think types can be both frustrating and life-saving. However, the "danger" for me lies primarily in implicit conversion. That is, Python vs Lua/JS/R. When writing large programs, some things happen implicitly and linting may not catch it. Everything else besides implicit conversion just helps structure the programs in specific ways and helps speed them up.
seanwilson 10y ago
Great overview article but I have a comment. > In Idris, we can say "the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument": > If we try to call this function as add 2 1, where the first argument is larger than the second, then the compiler will reject the program at compile time. > Haskell has no equivalent of the Idris type above, and Go has no equivalent of either the Idris type or the Haskell type. As a result, Idris can prevent many bugs that Haskell can't, and Haskell can prevent many bugs that Go can't. In both cases, we need additional type system features, which make the language more complex. I really wish when people talk about dependently typed programming languages (e.g. Idris, Coq, Agda, ATS), they would mention the effort involved to get these compile time checks to happen. These languages allow you to capture almost any program property you can think of as a type. Instead of being limited to saying function F "returns a number/list/string" like common type systems, you can capture arbitrarily complex properties like "F returns an even number", "F returns a permutation of the input list", "F always halts" or "F returns a proof of Fermat's Last Theorem". You don't get this for free and you have to help the computer verify these. Proving F matches the type is arbitrary hard and is impossible to automated in general (e.g. the halting problem tells us we cannot always tell if a function halts). For example, consider the type "F returns a sorted permutation of the input list", where F could be an implementation of bubble sort, quicksort, merge sort, radix sort or something even more complex. Each algorithm will require a different and potentially complex proof and most of the time the programmer needs to help the computer find the proof. It's completely unlike what people are used to from type systems and is an even more massive leap than for someone moving from the type systems of e.g. C++/Java to Haskell. I'm glad people are more aware of dependently typed languages but I feel the immense jump in how practical they are to use is severely overlooked.
- tomp 10y ago
  > Proving F matches the type is arbitrary hard and is impossible to automated in general So what? Even proving that array indices are not accessed out of bounds within loops would be a considerable leap in the state of the art of industrial programming languages. For most cases (i.e. linear integer arithmetics), that's always automatically (dis-)provable. We have to start somewhere...
NhanH 10y ago
The article is mainly focused on static typing. I guess it makes sense since the title is "Types". Although reading this, you might just think that dynamic typing is good for nothing. The more practical part of the article is great. However, the theoretical part could use some works. Especially the terminology isn't actually clear. Takes some example, what is "memory-safe" ? The only example makes it sounds like bound checking. And what does "no way to escape the language's type rules" mean? There are some usages of "valid program" and "invalid program" that makes my spider sense tingling as well. > However, no dynamic language can match the speed of carefully written static code in a language like Rust. > Any blanket statement of the form "static languages are better at x than dynamic languages" is almost certainly nonsense. Those two quoted statements come from the article. The section "Arguments for static and dynamic types" didn't mention a single reason why dynamic typing could be preferable over static-typing. It could at least have mentioned macro, or hand-waving claim that dynamic typing makes for prettier code at time (I think the author of python's requests library made that argument in one of the blog post). I think the last part should be removed (ranking the language by their typed system power). > There's a clear trend toward more powerful systems over time, especially when judging by language popularity rather than languages simply existing. Well, it looks true since we didn't consider any dynamic language at all... Focusing more on the "Concrete examples of type system power differences" would have been better for the article, I think. Something along the line of an example of Non-nullable type with something simple in TS, to optional/maybe monad, then dependent type that you can implement matrix multiplication (m * n) with (n * p) and got the type (m * p) back.
- hawski 10y ago
  >> However, no dynamic language can match the speed of carefully written static code in a language like Rust. >> Any blanket statement of the form "static languages are better at x than dynamic languages" is almost certainly nonsense. > Those two quoted statements come from the article. I think author had in mind "ALL static languages are better at x than ALL dynamic languages" as a nonsense. He probably didn't have in mind that "A static language_ IS better at x than A dynamic language_" is a nonsense.
- epidemian 10y ago
junke 10y ago
1 + eval(read_from_the_network()) > If we get an integer, that expression is fine; if we get a string, it's not. We can't know what we'll get until we actually run, so we can't statically analyze the type. > The unsatisfying solution used in practice is to give eval() the type Any, which is like Object in some OO languages or interface {} in Go: it's the type that can have any value. Values of type Any aren't constrained in any way, so this effectively removes the type system's ability to help us with code involving eval. Languages with both eval and a type system have to abandon type safety whenever eval is used. No, you can give EVAL a returning type of any (T) but still make type inference work. (+ 1 (eval (read))) The meaning of a type in SBCL is: if an expression evaluates without error, then its type is .... In other words, the type of the above expression is NUMBER. There is also a NIL type (bottom) which represent the empty set of values. If a function has a return type of NIL, it means that it does not return a value normally. This is the case for the ERROR function, or the (LOOP) expression.
- evincarofautumn 10y ago
  > if an expression evaluates without error, then its type is… What’s curious is that this is true in every language with general recursion/looping: int f(int n) { while (true) {} return n + 1; } (In other words, the type of “f” isn’t the logical formula “a → a”, but rather “a → ¬¬a”.) The type of “eval” can also be fully static; it can just return a type that you have to do case analysis or runtime type inspection on to use. In Haskell, with a data type: data Value = Integer Int | Text String | ... eval :: String -> Value foo = do value <- read_from_the_network let result = eval value case result of Integer n -> return (1 + n) _ -> error "that was not an integer!" Or with RTTI: eval :: String -> Dynamic foo = do value <- read_from_the_network let result = eval value case fromDynamic result of Just n -> return (1 + n) Nothing -> error "that was not an integer!" “fromDynamic” has the type: Typeable a => Dynamic -> Maybe a Which is to say “given a dynamic value, and its runtime type information, I can either give you the value back with a static type, or nothing if I can’t perform the downcast”—much like “dynamic_cast” on pointer types in C++.
  - 10y ago
titanomachy 10y ago
Someone who has experience with both Agda and Idris, could you comment on which is easier to get started with? Coming from a Haskell background, I'd like to try my hand at writing more interesting constraints into my types. Any experiences using these languages for (non-research) work? I've played around with Coq a little and it certainly feels more like a proof assistant than a programming language. It was fairly confusing and unfamiliar, but interesting nonetheless. Something with slightly more traditional ergonomics might be easier to pick up.
- seanwilson 10y ago
  > Someone who has experience with both Agda and Idris, could you comment on which is easier to get started with? Coming from a Haskell background, I'd like to try my hand at writing more interesting constraints into my types. Any experiences using these languages for (non-research) work? The learning curve is almost vertical to be completely honest from personal experience. I find most tutorials are written by people with a strong background in logic, type systems and mathematics, so it's a struggle to rely only on your knowledge of mainstream programming languages as you're learning lots of new things at once (e.g. formal proofs, formal specifications, logic, pure functional programming). It's a super interesting area if you can stick with it though so keep at it!
  - titanomachy 10y ago
    > most tutorials are written by people with a strong background in logic, type systems, and mathematics... I'm a little used to this from Haskell, although I imagine the dependently-typed languages are even worse in that regard. Working through the Idris tutorial now and at least the syntax is familiar.
    - seanwilson 10y ago
      > I'm a little used to this from Haskell, although I imagine the dependently-typed languages are even worse in that regard. Working through the Idris tutorial now and at least the syntax is familiar. That's what I mean by the difficultly jump. Like when you go from C++ to Java or the other way around, there's a lot of familiar things to cling on to while you make the transition. With dependently typed languages, there's a massive pile of unfamiliar stuff so the steep learning curve is unavoidable really. Someone needs to write a "dependently typed programming for Java programmers guide". :)
DSMan195276 10y ago
Being someone who enjoys C (Though I readily admit the type system is generally weak compared to the others on the list) there's a little misinformation on this page that I think it worth clearing up - though I think the majority of the information is still perfectly good: C does not 'allow' you to do a lot of the things mentioned on this page, it just doesn't generally carry around all the information to check and make sure you don't. So the page is generally still right - it can be fairly easy to get memory-unsafe things past the compiler - though whether you want to blame the type-system or blame the compiler could be debated, probably a bit of both. Reading past the ends of arrays is illegal, as is accessing a variable of one type through a pointer to another type. Some of these things will get checked or assumed by the compiler (And thus break code that does these things, and in some ways break them in subtle ways), but there's no guarantee that the compiler actually knows you broke the rules. This tends to be the main different from other languages like Java, where the compiler/run-time does carry around such information and thus can do such checks and does know you when you broke the rules. With that said, while there are some things I don't like about the design of Rust overall, giving the compiler more information to be able to figure out the above is definitely one thing they did right in comparison to C. The problem C is approaching is that, even though compilers are getting smarter, enough code was already written before that was the case to result in breaking when you attempt to use 'smarter' compilers.
- naasking 10y ago
  Since this articles is about types, any behaviour the compiler doesn't check or doesn't generate a type error is "allowed".
  - DSMan195276 10y ago
    The issue with that idea is that there is more than one C compiler. Some of them issue no warnings at all, and some of them (like `gcc`) will yell at you and probably break your code if you attempt to do some of the things I outlined. I disagree with saying it is 'allowed' by the type system, because a smart C compiler could throw out your code and refuse to compile it if you do such things, and in doing so would still be within the C standard. Some work has already been done on this front in `gcc` (And I would assume `clang`) - the issue tends to be that by doing this, you end-up breaking some older code that used to work fine. And since older compilers didn't enforce these rules, people aren't as aware of them.
wz1000 10y ago
add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat add x y = x + y Actually, (GHC) Haskell can express something like this type if you turn on the required extensions. data Nat = Z | S Z deriving (Eq, Ord, Show) data SNat (n :: Nat) where SZ :: SNat Z SS :: SNat n -> SNat (S n) type family Compare (a :: Nat) (b :: Nat) :: Ordering where Compare Z Z = EQ Compare (S a) Z = GT Compare Z (S a) = LT Compare (S a) (S b) = Compare a b type a < b = Compare a b ~ LT type family (+) (a :: Nat) (b :: Nat) :: Nat where Z + a = a a + Z = a (S a) + b = S (a + b) add :: (a < b) => SNat a -> SNat b -> SNat (a+b) add = ...
DanWaterworth 10y ago
> Haskell has no equivalent of the Idris type above, and Go has no equivalent of either the Idris type or the Haskell type. As a result, Idris can prevent many bugs that Haskell can't, and Haskell can prevent many bugs that Go can't. In both cases, we need additional type system features, which make the language more complex. Type checking Idris is much simpler than Haskell.
- gary_bernhardt 10y ago
  It doesn't say "type checking", though. It says "the language", which I think of as including the respective preludes.
  - jroesch 10y ago
    The core theory (and implementation) is much simpler for almost all dependent type theories. At least this is my personal feeling after having read a lot of GHC code, written an Idris backend, the native backend for Lean, and significant portions of `rustc`.
    - gary_bernhardt 10y ago
      It's generally (or maybe universally) more difficult to "get" dependent typing than plain old ML-family static typing. I mean, this HN comments page alone has multiple threads where people don't think that the "x > y" proof example even works. For most programmers, that's how non-obvious the possibility of proving nontrivial properties of code is. Maybe I should change the wording in the OP to make it clear that I'm talking about the set of ideas required to use the language, not the characters that need to be typed into a computer to make it work.
      - DanWaterworth 10y ago
        > It's generally (or maybe universally) more difficult to "get" dependent typing than plain old ML-family static typing. That's true, but Haskell has come a long way since a direct comparison like that would make sense. > I mean, this HN comments page alone has multiple threads where people don't think that the "x > y" proof example even works. I think this is because people have some preconceived idea about what dependent typing is before they come to dependently typed languages. So, not only are they learning about dependent types, but they are also fighting their preconceived notions. That was certainly the case for me. It's an interesting facet of the human condition; every time we learn a new tool, we have to be reminded that it's not magic. Now, having become proficient, I have a better intuition for how to get my complex Idris programs to type check than my complex Haskell ones. Idris is actually simpler, it's not just about line counts.
kpmah 10y ago
I wrote a little article, which has been posted here before, that shows the power of different type systems and what kind of bugs you can expect to prevent: http://kevinmahoney.co.uk/articles/tests-vs-types/ http://kevinmahoney.co.uk/articles/tests-vs-types/
arianvanp 10y ago
> If we try to call this function as add 2 1, where the first argument is larger than the second, then the compiler will reject the program at compile time This is not entirely true in general. auto is only a best bet. It might not be able to prove something right and will fail. For example, if it has to recurse deeper than 100 constructors. In this case, the user of the function has to provide a proof himself. See it as a bloom filter. if it doesn't fail, you're sure your function is correctly called. if it does fail, it might still be correctly called but the compiler just didn't have enough time to prove it. In that case a user needs to convince the compiler that he is right.
- gary_bernhardt 10y ago
  I don't see the problem here. I said that Idris will reject the program if the proof fails. That's what you're saying too, unless I'm very confused. (It's late, so maybe I am?)
  - arianvanp 10y ago
    Yes, but it might also reject correct programs. that's the point I'm trying to make.
    - gary_bernhardt 10y ago
      That doesn't contradict the quote that you provided. The quote just says "the compiler will reject the program at compile time [if there's no valid proof]", which is true.
ozy 10y ago
So what might make dynamic languages easier to write in? I enjoy dynamic languages more because: * "double kilometerToMiles(double km) { return km / 1.6 }" here the types are of really low value, yet I have to type them in. * a mutable list of generic and variable arity event handlers. Really hard to specify as a type (most languages cannot do it). Really easy to use. * co- and contravariance and lists, the math works exactly opposite of intuition. * when you change your mind on the types/arity beyond what your IDE can follow, it is a lot of low value work * if your test suite has 100% coverage of arguments/return-value and field usage, you have type checked your program. If I am going to write down types, they better be of value to me. Like types that are null or non-null, or tainted (from the user) or non-tainted. Or two numbers that are kilometers vs miles. Or only accessible under a certain lock or other preconditions. And be flow sensitive (kotlin style null checks), not make me write even more code. But if you are a dynamic language, do be strong typed (no "1" == 1). Also be dynamic in arity, that is (part-of) a type. Don't be handwavy scoped, lexical scoping is probably the only predictable way to do scoping. Fail fast, like prevent spelling mistakes for non existing field names for example. And allow this to work: "2 * Vector(10,10)". And from that perspective there is still quite some room for improvement in all classes of languages, I suppose, and good that there is lot of movement and experiments today.
- lucian1900 10y ago
  Writing down the types isn't a necessary property of static type systems. In Haskell, F# or (OCa)ML, you almost never have to actually mention any types. I do agree that Java-style types aren't of much value. That catches few errors at significant cost.
  - MrBuddyCasino 10y ago
    Catching logical errors is only one out of several things that static typing gives you. Incidentally, right now this is a few positions above this posting: https://news.ycombinator.com/item?id=12350063 https://news.ycombinator.com/item?id=12350063 Better IDE support, a kind of self-documentation and increased performance come to mind. I know there are counter-examples for each of these points, but the general trend cannot be denied.
one-more-minute 10y ago
If this topic interests you, Julia's type system is worth checking out [1]. Julia is unusual among dynamic languages not just for having a powerful type system (including parametric types), but also for making it idiomatic to make full use of types. Aside from the benefits to the programmer, this also allows the compiler to get to Rust-level performance where it's needed. I find that this is a nice compromise that gets a lot of the benefits of static type systems (small, local errors as opposed to behavioural bugs, ability to express concepts and constraints) without the drawbacks (loss of interactivity, or inability to escape the type system when it's appropriate). [1]: http://docs.julialang.org/en/latest/manual/types/ http://docs.julialang.org/en/latest/manual/types/
- lmm 10y ago
  It sounds very ad-hoc? (And Julia's benchmarking has not been reputable in the past, FWIW). > without the drawbacks (loss of interactivity, or inability to escape the type system when it's appropriate). One can absolutely have interactivity in a statically typed language, and virtually all statically typed languages support casting when you absolutely need to.
  - one-more-minute 10y ago
    "Ad-hoc" seems subjective but to me it feels very carefully thought out. And while I've found the benchmarks to be accurate, I more importantly mean myself (and many others I know) being easily able to get high performance code when we need it. My second paragraph was only a personal take on what works for me, so YMMV, but nevertheless: I'm not arguing against static type systems in principle, but these are practical concerns rather than theoretical ones. I don't know of a mainstream static language that supports a fully dynamic REPL (Haskell's isn't great) and casting back and forth to `interface{}`, `Object`, or `Any` everywhere is a huge overhead compared to duck typing. I look forward to a future language solving those issues, but that's not the case today.
    - lmm 10y ago
      > "Ad-hoc" seems subjective but to me it feels very carefully thought out. I guess I'd like to see a simple formalism. > myself (and many others I know) being easily able to get high performance code when we need it. That's true for a lot of languages. It doesn't make it Rust-level. > I'm not arguing against static type systems in principle, but these are practical concerns rather than theoretical ones. I don't know of a mainstream static language that supports a fully dynamic REPL (Haskell's isn't great) and casting back and forth to `interface{}`, `Object`, or `Any` everywhere is a huge overhead compared to duck typing. I look forward to a future language solving those issues, but that's not the case today. Shrug, not my experience. I don't know what you mean by "fully generic", but I've been very happy with the Scala REPL - I've never once thought "this would be easy in the Python REPL but I can't do it because of the type system". Casting is indeed a big overhead if you're doing it everywhere, but my experience is the cases where you need it are extremely rare.
amelius 10y ago
> A type is a collection of possible values Ok, but do two collections with the same values always correspond to the same type?
- kd0amg 10y ago
  It depends on the language. If you have, for example, a type-and-effect system, a type can contain information (like "we wrote to stdout while computing this") that is never reflected in the value itself. In a formal setting, it's more appropriate to describe a type as a collection of pieces of source code, so that `2+3` and `print "computing...\n"; 2+3` have different types even though they'll evaluate to the same thing.
- paulddraper 10y ago
  Yes, but if remember you can always say that the values are different. A blue 5, and a red 5. Five feet, or five inches.
- munificent 10y ago
  Yes, they do.
- acjohnson55 10y ago
  Generally, no, at least with nominal typing.
naasking 10y ago
Decent overview of many concepts, but the opening line isn't strictly true: > A type is a collection of possible values. A type is a proposition, and "This binding has one of these possible values" is merely one type of proposition. So a type is much more powerful than a simple set-based interpretation, even though this is how most people think about it. For instance, in Haskell you can encode a region calculus that ensures prompt reclamation of file handles and other scarce resources [1]. The relations between nested regions to ensure correctness seems awkward to interpret as a set, but it's straightforward if you just think of types as a relation. [1] http://okmij.org/ftp/Haskell/regions.html#light-weight http://okmij.org/ftp/Haskell/regions.html#light-weight
- chriswarbo 10y ago
  Well, there are several ways to think about types, especially regarding this article, which tries to cover static and dynamic types. Most formal definitions/treatments of types I've come across do not apply to dynamic types at all; usually the typing formalism says nothing about dynamically typed programs/values other than giving them one big recursive type. What we would informally call "dynamic types" are then treated completely separately, e.g. via "tags". While such distinctions are certainly useful, an introductory/broad-overview explanation like this seems to benefit without such complications/distractions.
  - naasking 10y ago
    > While such distinctions are certainly useful, an introductory/broad-overview explanation like this seems to benefit without such complications/distractions. I don't think misrepresenting types is the way to go. An introduction like I just gave seems simple enough, where a type is a proposition about a program, and you just then explain that most such propositions are "variable X may take on values from set Y". It's important not to perpetuate the false notion that sets of simple sets of values suffice to explain types, because it entails the common and equally false notion that full test coverage in a dynamically typed language suffices to match the safety of a statically typed language.
    - 10y ago
levbrie 10y ago
Kind of shocked nobody mentioned this, even if it is a bit of an aside, but umm, I've been dying for anything at all from Gary Bernhardt - I don't even know what to say except that it makes me hope however unrealistically that will one day get something like the magnum opus that is "Destroy All Software" from him again.
- dochtman 10y ago
  You know he just started to post new stuff, right? https://www.destroyallsoftware.com/screencasts/catalog https://www.destroyallsoftware.com/screencasts/catalog
  - deleted 10y ago
    [deleted]
  - levbrie 10y ago
    I know. Mind blown.
- nickpsecurity 10y ago
  I havent read/seen it. Im guessing you know more than Id see in an abstract. So, what's the significance of that work?
athenot 10y ago
I've been very curious about Perl6's gradual typing[1] which, as I understand it, draws a lot from Haskell's type system but in an optional manner. subset NonNegativeInt of Int where * >= 0; sub fib(NonNegativeInt $nth) { given $nth { when 0 { 0 } when 1 { 1 } default { fib($nth-1) + fib($nth-2) } } } [1] http://blogs.perl.org/users/ovid/2015/02/avoid-a-common-software-bug-by-using-perl-6.html http://blogs.perl.org/users/ovid/2015/02/avoid-a-common-soft...
zeveb 10y ago
> The unsatisfying solution used in practice is to give eval() the type Any, which is like Object in some OO languages or interface {} in Go: it's the type that can have any value. Values of type Any aren't constrained in any way, so this effectively removes the type system's ability to help us with code involving eval. Languages with both eval and a type system have to abandon type safety whenever eval is used. It's not quite true that they must abandon type safety: rather, they must abandon a certain kind of compile-time type check. It's not unsafe to use eval or Any values (i.e., it won't crash the system); one must simply examine the Any value (at runtime, natch) and do stuff with it.
eximius 10y ago
So, how do these advanced types work? For their `add` example, I imagine just having x<y somewhere is sufficient. But let's say I write a sorting implementation but the compiler can't quite figure out that it is correct. Is there a provided way to tell the compiler 'trust me, this property is now true'? Also, I'm assuming the compiler has two classes of errors here: a counter example vs. unable to prove? Can anyone point me to documentation on these (in Idris, preferably)?
- icen 10y ago
  In Idris, there are functions `believe_me` and `really_believe_me`, which assert things to the compiler. They're generally only used for FFI code, or for extremely tedious proofs. If you wanted to prove that a list was sorted, you'd write another datatype: IsSorted : Ord a => List a -> Type which represents the proposition that the input list is sorted. You could encode this by requiring that any new element in the list is either the first element, or less than or equal to the previous element. Then, your sorting function could return a dependent pair: (l : List a ** IsSorted l) which can be read as the list, accompanied by a proof that it is, in fact, sorted. Since your `IsSorted` type requires that the list is sorted, via construction, you won't be able to supply the output of the function unless your code is correct (or you use `believe_me`!). The compiler doesn't generally come up with counterexamples for you; with this style, if the proof isn't complete, it won't compile.
mamcx 10y ago
I read that type checking is easier with dependent types. I'm barely aware of adga adn other langs that are used for profs, but wonder how useful (and what danger ahead) could cause to design a language with this for more mundane purposes (like, for example, build websites, data manipulation, gui, etc)
rpazyaquian 10y ago
What types are and what they do is all well and good, but what I want to know is how they would help me write a larger application. Would it help it be more correct, be written faster, or be more flexible? Does it just help on a line-by-line programming basis, or can it have any ramifications on a higher level like product design?

Types

445 points by ivank 10y ago

th0ma5 10y ago

Hope this makes it into Wikipedia instead of here.

paulddraper 10y ago
It'll get moderated out.
- NhanH 10y ago
  For this article specifically, it shouldn't be on wiki. The quality still needs a lot of polish, and too much opinions.
  - gary_bernhardt 10y ago
    This is a decent summary of why I'm doing it. Wikipedia is full of "high quality" content, where "high quality" means "directly exposing every detail that anyone ever thought to nitpick", and this topic is a nitpicker's paradise. There's value in that detail-heavy style, but it's difficult to learn from and it's a type of writing that I rarely want to read. As for opinions (and lack thereof), they prevent Wikipedia from saying many things that are both well-known and easily stated. The lack of clear summaries of widespread disagreeing opinions keeps our implicit knowledge implicit.
    - NhanH 10y ago
      I agree with your reasoning and your description of Wikipedia. However, despite all the flaws, wiki is reasonably helpful, and I doubt filling it with more opinions would be helping the case.

twblalock 10y ago

The Idris example seems to need further explanation: > In Idris, we can say "the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument": > add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat > add x y = x + y That's all well and good, if you know the values of x and y at compile time. Consider a program that reads x and y from STDIN. The user could provide an x that is equal to or larger than y (or could provide only one value, or values that are not numbers). I see no way to deal with that except to throw a runtime error. Is that what would happen?

platz 10y ago
not in idris, because it would force you to do that check manually and pass in the evidence as proof. it has a bunch of tools to help you do this.. namely lifting values into types with 'dependent pairs'. idris doesnt automagically calculate everything for you, but makes sure at compile time, that you provide evidence at run time for the things you have asserted in the types. it makes more sense after going through some of the tutorials and books.
NhanH 10y ago
I do NOT know anything about Idris, but I'd imagine you have to do a check along the line of `if (x<y) then` before being able to call `add`, within that block-scope, the compiler should be able to infer that x<y. Typescript has something similar, where if you do `if (foo)`, the compiler will know that foo can't be null or undefined.
_ibu9 10y ago
The missing explanation is that `smaller` is a third argument to the function. It's type is a proof that x <= y. Since it is in curly brackets with the auto keyword, the compiler will fill in this proof in many cases, like when the values are statically known. In the case where the values are read from the external environment, first you would have to compare them before calling the function. The comparator would return either a proof that x <= y, or x > y. In the first case you plug that value into the `smaller` argument, in the second case it's your responsibility to signal whatever kind of application-specific error is appropriate (assuming x > y is some kind of erroneous condition).

lqdc13 10y ago

I think types can be both frustrating and life-saving. However, the "danger" for me lies primarily in implicit conversion. That is, Python vs Lua/JS/R. When writing large programs, some things happen implicitly and linting may not catch it. Everything else besides implicit conversion just helps structure the programs in specific ways and helps speed them up.

seanwilson 10y ago

Great overview article but I have a comment. > In Idris, we can say "the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument": > If we try to call this function as add 2 1, where the first argument is larger than the second, then the compiler will reject the program at compile time. > Haskell has no equivalent of the Idris type above, and Go has no equivalent of either the Idris type or the Haskell type. As a result, Idris can prevent many bugs that Haskell can't, and Haskell can prevent many bugs that Go can't. In both cases, we need additional type system features, which make the language more complex. I really wish when people talk about dependently typed programming languages (e.g. Idris, Coq, Agda, ATS), they would mention the effort involved to get these compile time checks to happen. These languages allow you to capture almost any program property you can think of as a type. Instead of being limited to saying function F "returns a number/list/string" like common type systems, you can capture arbitrarily complex properties like "F returns an even number", "F returns a permutation of the input list", "F always halts" or "F returns a proof of Fermat's Last Theorem". You don't get this for free and you have to help the computer verify these. Proving F matches the type is arbitrary hard and is impossible to automated in general (e.g. the halting problem tells us we cannot always tell if a function halts). For example, consider the type "F returns a sorted permutation of the input list", where F could be an implementation of bubble sort, quicksort, merge sort, radix sort or something even more complex. Each algorithm will require a different and potentially complex proof and most of the time the programmer needs to help the computer find the proof. It's completely unlike what people are used to from type systems and is an even more massive leap than for someone moving from the type systems of e.g. C++/Java to Haskell. I'm glad people are more aware of dependently typed languages but I feel the immense jump in how practical they are to use is severely overlooked.

tomp 10y ago
> Proving F matches the type is arbitrary hard and is impossible to automated in general So what? Even proving that array indices are not accessed out of bounds within loops would be a considerable leap in the state of the art of industrial programming languages. For most cases (i.e. linear integer arithmetics), that's always automatically (dis-)provable. We have to start somewhere...

NhanH 10y ago

The article is mainly focused on static typing. I guess it makes sense since the title is "Types". Although reading this, you might just think that dynamic typing is good for nothing. The more practical part of the article is great. However, the theoretical part could use some works. Especially the terminology isn't actually clear. Takes some example, what is "memory-safe" ? The only example makes it sounds like bound checking. And what does "no way to escape the language's type rules" mean? There are some usages of "valid program" and "invalid program" that makes my spider sense tingling as well. > However, no dynamic language can match the speed of carefully written static code in a language like Rust. > Any blanket statement of the form "static languages are better at x than dynamic languages" is almost certainly nonsense. Those two quoted statements come from the article. The section "Arguments for static and dynamic types" didn't mention a single reason why dynamic typing could be preferable over static-typing. It could at least have mentioned macro, or hand-waving claim that dynamic typing makes for prettier code at time (I think the author of python's requests library made that argument in one of the blog post). I think the last part should be removed (ranking the language by their typed system power). > There's a clear trend toward more powerful systems over time, especially when judging by language popularity rather than languages simply existing. Well, it looks true since we didn't consider any dynamic language at all... Focusing more on the "Concrete examples of type system power differences" would have been better for the article, I think. Something along the line of an example of Non-nullable type with something simple in TS, to optional/maybe monad, then dependent type that you can implement matrix multiplication (m * n) with (n * p) and got the type (m * p) back.

hawski 10y ago
>> However, no dynamic language can match the speed of carefully written static code in a language like Rust. >> Any blanket statement of the form "static languages are better at x than dynamic languages" is almost certainly nonsense. > Those two quoted statements come from the article. I think author had in mind "ALL static languages are better at x than ALL dynamic languages" as a nonsense. He probably didn't have in mind that "A static language_ IS better at x than A dynamic language_" is a nonsense.
epidemian 10y ago

junke 10y ago

1 + eval(read_from_the_network()) > If we get an integer, that expression is fine; if we get a string, it's not. We can't know what we'll get until we actually run, so we can't statically analyze the type. > The unsatisfying solution used in practice is to give eval() the type Any, which is like Object in some OO languages or interface {} in Go: it's the type that can have any value. Values of type Any aren't constrained in any way, so this effectively removes the type system's ability to help us with code involving eval. Languages with both eval and a type system have to abandon type safety whenever eval is used. No, you can give EVAL a returning type of any (T) but still make type inference work. (+ 1 (eval (read))) The meaning of a type in SBCL is: if an expression evaluates without error, then its type is .... In other words, the type of the above expression is NUMBER. There is also a NIL type (bottom) which represent the empty set of values. If a function has a return type of NIL, it means that it does not return a value normally. This is the case for the ERROR function, or the (LOOP) expression.

evincarofautumn 10y ago
> if an expression evaluates without error, then its type is… What’s curious is that this is true in every language with general recursion/looping: int f(int n) { while (true) {} return n + 1; } (In other words, the type of “f” isn’t the logical formula “a → a”, but rather “a → ¬¬a”.) The type of “eval” can also be fully static; it can just return a type that you have to do case analysis or runtime type inspection on to use. In Haskell, with a data type: data Value = Integer Int | Text String | ... eval :: String -> Value foo = do value <- read_from_the_network let result = eval value case result of Integer n -> return (1 + n) _ -> error "that was not an integer!" Or with RTTI: eval :: String -> Dynamic foo = do value <- read_from_the_network let result = eval value case fromDynamic result of Just n -> return (1 + n) Nothing -> error "that was not an integer!" “fromDynamic” has the type: Typeable a => Dynamic -> Maybe a Which is to say “given a dynamic value, and its runtime type information, I can either give you the value back with a static type, or nothing if I can’t perform the downcast”—much like “dynamic_cast” on pointer types in C++.
- 10y ago

titanomachy 10y ago

Someone who has experience with both Agda and Idris, could you comment on which is easier to get started with? Coming from a Haskell background, I'd like to try my hand at writing more interesting constraints into my types. Any experiences using these languages for (non-research) work? I've played around with Coq a little and it certainly feels more like a proof assistant than a programming language. It was fairly confusing and unfamiliar, but interesting nonetheless. Something with slightly more traditional ergonomics might be easier to pick up.

seanwilson 10y ago
> Someone who has experience with both Agda and Idris, could you comment on which is easier to get started with? Coming from a Haskell background, I'd like to try my hand at writing more interesting constraints into my types. Any experiences using these languages for (non-research) work? The learning curve is almost vertical to be completely honest from personal experience. I find most tutorials are written by people with a strong background in logic, type systems and mathematics, so it's a struggle to rely only on your knowledge of mainstream programming languages as you're learning lots of new things at once (e.g. formal proofs, formal specifications, logic, pure functional programming). It's a super interesting area if you can stick with it though so keep at it!
- titanomachy 10y ago
  > most tutorials are written by people with a strong background in logic, type systems, and mathematics... I'm a little used to this from Haskell, although I imagine the dependently-typed languages are even worse in that regard. Working through the Idris tutorial now and at least the syntax is familiar.
  - seanwilson 10y ago
    > I'm a little used to this from Haskell, although I imagine the dependently-typed languages are even worse in that regard. Working through the Idris tutorial now and at least the syntax is familiar. That's what I mean by the difficultly jump. Like when you go from C++ to Java or the other way around, there's a lot of familiar things to cling on to while you make the transition. With dependently typed languages, there's a massive pile of unfamiliar stuff so the steep learning curve is unavoidable really. Someone needs to write a "dependently typed programming for Java programmers guide". :)

DSMan195276 10y ago

Being someone who enjoys C (Though I readily admit the type system is generally weak compared to the others on the list) there's a little misinformation on this page that I think it worth clearing up - though I think the majority of the information is still perfectly good: C does not 'allow' you to do a lot of the things mentioned on this page, it just doesn't generally carry around all the information to check and make sure you don't. So the page is generally still right - it can be fairly easy to get memory-unsafe things past the compiler - though whether you want to blame the type-system or blame the compiler could be debated, probably a bit of both. Reading past the ends of arrays is illegal, as is accessing a variable of one type through a pointer to another type. Some of these things will get checked or assumed by the compiler (And thus break code that does these things, and in some ways break them in subtle ways), but there's no guarantee that the compiler actually knows you broke the rules. This tends to be the main different from other languages like Java, where the compiler/run-time does carry around such information and thus can do such checks and does know you when you broke the rules. With that said, while there are some things I don't like about the design of Rust overall, giving the compiler more information to be able to figure out the above is definitely one thing they did right in comparison to C. The problem C is approaching is that, even though compilers are getting smarter, enough code was already written before that was the case to result in breaking when you attempt to use 'smarter' compilers.

naasking 10y ago
Since this articles is about types, any behaviour the compiler doesn't check or doesn't generate a type error is "allowed".
- DSMan195276 10y ago
  The issue with that idea is that there is more than one C compiler. Some of them issue no warnings at all, and some of them (like `gcc`) will yell at you and probably break your code if you attempt to do some of the things I outlined. I disagree with saying it is 'allowed' by the type system, because a smart C compiler could throw out your code and refuse to compile it if you do such things, and in doing so would still be within the C standard. Some work has already been done on this front in `gcc` (And I would assume `clang`) - the issue tends to be that by doing this, you end-up breaking some older code that used to work fine. And since older compilers didn't enforce these rules, people aren't as aware of them.

wz1000 10y ago

add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat add x y = x + y Actually, (GHC) Haskell can express something like this type if you turn on the required extensions. data Nat = Z | S Z deriving (Eq, Ord, Show) data SNat (n :: Nat) where SZ :: SNat Z SS :: SNat n -> SNat (S n) type family Compare (a :: Nat) (b :: Nat) :: Ordering where Compare Z Z = EQ Compare (S a) Z = GT Compare Z (S a) = LT Compare (S a) (S b) = Compare a b type a < b = Compare a b ~ LT type family (+) (a :: Nat) (b :: Nat) :: Nat where Z + a = a a + Z = a (S a) + b = S (a + b) add :: (a < b) => SNat a -> SNat b -> SNat (a+b) add = ...

DanWaterworth 10y ago

> Haskell has no equivalent of the Idris type above, and Go has no equivalent of either the Idris type or the Haskell type. As a result, Idris can prevent many bugs that Haskell can't, and Haskell can prevent many bugs that Go can't. In both cases, we need additional type system features, which make the language more complex. Type checking Idris is much simpler than Haskell.

gary_bernhardt 10y ago
It doesn't say "type checking", though. It says "the language", which I think of as including the respective preludes.
- jroesch 10y ago
  The core theory (and implementation) is much simpler for almost all dependent type theories. At least this is my personal feeling after having read a lot of GHC code, written an Idris backend, the native backend for Lean, and significant portions of `rustc`.
  - gary_bernhardt 10y ago
    It's generally (or maybe universally) more difficult to "get" dependent typing than plain old ML-family static typing. I mean, this HN comments page alone has multiple threads where people don't think that the "x > y" proof example even works. For most programmers, that's how non-obvious the possibility of proving nontrivial properties of code is. Maybe I should change the wording in the OP to make it clear that I'm talking about the set of ideas required to use the language, not the characters that need to be typed into a computer to make it work.
    - DanWaterworth 10y ago
      > It's generally (or maybe universally) more difficult to "get" dependent typing than plain old ML-family static typing. That's true, but Haskell has come a long way since a direct comparison like that would make sense. > I mean, this HN comments page alone has multiple threads where people don't think that the "x > y" proof example even works. I think this is because people have some preconceived idea about what dependent typing is before they come to dependently typed languages. So, not only are they learning about dependent types, but they are also fighting their preconceived notions. That was certainly the case for me. It's an interesting facet of the human condition; every time we learn a new tool, we have to be reminded that it's not magic. Now, having become proficient, I have a better intuition for how to get my complex Idris programs to type check than my complex Haskell ones. Idris is actually simpler, it's not just about line counts.

kpmah 10y ago

I wrote a little article, which has been posted here before, that shows the power of different type systems and what kind of bugs you can expect to prevent: http://kevinmahoney.co.uk/articles/tests-vs-types/ http://kevinmahoney.co.uk/articles/tests-vs-types/

arianvanp 10y ago

> If we try to call this function as add 2 1, where the first argument is larger than the second, then the compiler will reject the program at compile time This is not entirely true in general. auto is only a best bet. It might not be able to prove something right and will fail. For example, if it has to recurse deeper than 100 constructors. In this case, the user of the function has to provide a proof himself. See it as a bloom filter. if it doesn't fail, you're sure your function is correctly called. if it does fail, it might still be correctly called but the compiler just didn't have enough time to prove it. In that case a user needs to convince the compiler that he is right.

gary_bernhardt 10y ago
I don't see the problem here. I said that Idris will reject the program if the proof fails. That's what you're saying too, unless I'm very confused. (It's late, so maybe I am?)
- arianvanp 10y ago
  Yes, but it might also reject correct programs. that's the point I'm trying to make.
  - gary_bernhardt 10y ago
    That doesn't contradict the quote that you provided. The quote just says "the compiler will reject the program at compile time [if there's no valid proof]", which is true.

ozy 10y ago

So what might make dynamic languages easier to write in? I enjoy dynamic languages more because: * "double kilometerToMiles(double km) { return km / 1.6 }" here the types are of really low value, yet I have to type them in. * a mutable list of generic and variable arity event handlers. Really hard to specify as a type (most languages cannot do it). Really easy to use. * co- and contravariance and lists, the math works exactly opposite of intuition. * when you change your mind on the types/arity beyond what your IDE can follow, it is a lot of low value work * if your test suite has 100% coverage of arguments/return-value and field usage, you have type checked your program. If I am going to write down types, they better be of value to me. Like types that are null or non-null, or tainted (from the user) or non-tainted. Or two numbers that are kilometers vs miles. Or only accessible under a certain lock or other preconditions. And be flow sensitive (kotlin style null checks), not make me write even more code. But if you are a dynamic language, do be strong typed (no "1" == 1). Also be dynamic in arity, that is (part-of) a type. Don't be handwavy scoped, lexical scoping is probably the only predictable way to do scoping. Fail fast, like prevent spelling mistakes for non existing field names for example. And allow this to work: "2 * Vector(10,10)". And from that perspective there is still quite some room for improvement in all classes of languages, I suppose, and good that there is lot of movement and experiments today.

lucian1900 10y ago
Writing down the types isn't a necessary property of static type systems. In Haskell, F# or (OCa)ML, you almost never have to actually mention any types. I do agree that Java-style types aren't of much value. That catches few errors at significant cost.
- MrBuddyCasino 10y ago
  Catching logical errors is only one out of several things that static typing gives you. Incidentally, right now this is a few positions above this posting: https://news.ycombinator.com/item?id=12350063 https://news.ycombinator.com/item?id=12350063 Better IDE support, a kind of self-documentation and increased performance come to mind. I know there are counter-examples for each of these points, but the general trend cannot be denied.

one-more-minute 10y ago

If this topic interests you, Julia's type system is worth checking out [1]. Julia is unusual among dynamic languages not just for having a powerful type system (including parametric types), but also for making it idiomatic to make full use of types. Aside from the benefits to the programmer, this also allows the compiler to get to Rust-level performance where it's needed. I find that this is a nice compromise that gets a lot of the benefits of static type systems (small, local errors as opposed to behavioural bugs, ability to express concepts and constraints) without the drawbacks (loss of interactivity, or inability to escape the type system when it's appropriate). [1]: http://docs.julialang.org/en/latest/manual/types/ http://docs.julialang.org/en/latest/manual/types/

lmm 10y ago
It sounds very ad-hoc? (And Julia's benchmarking has not been reputable in the past, FWIW). > without the drawbacks (loss of interactivity, or inability to escape the type system when it's appropriate). One can absolutely have interactivity in a statically typed language, and virtually all statically typed languages support casting when you absolutely need to.
- one-more-minute 10y ago
  "Ad-hoc" seems subjective but to me it feels very carefully thought out. And while I've found the benchmarks to be accurate, I more importantly mean myself (and many others I know) being easily able to get high performance code when we need it. My second paragraph was only a personal take on what works for me, so YMMV, but nevertheless: I'm not arguing against static type systems in principle, but these are practical concerns rather than theoretical ones. I don't know of a mainstream static language that supports a fully dynamic REPL (Haskell's isn't great) and casting back and forth to `interface{}`, `Object`, or `Any` everywhere is a huge overhead compared to duck typing. I look forward to a future language solving those issues, but that's not the case today.
  - lmm 10y ago
    > "Ad-hoc" seems subjective but to me it feels very carefully thought out. I guess I'd like to see a simple formalism. > myself (and many others I know) being easily able to get high performance code when we need it. That's true for a lot of languages. It doesn't make it Rust-level. > I'm not arguing against static type systems in principle, but these are practical concerns rather than theoretical ones. I don't know of a mainstream static language that supports a fully dynamic REPL (Haskell's isn't great) and casting back and forth to `interface{}`, `Object`, or `Any` everywhere is a huge overhead compared to duck typing. I look forward to a future language solving those issues, but that's not the case today. Shrug, not my experience. I don't know what you mean by "fully generic", but I've been very happy with the Scala REPL - I've never once thought "this would be easy in the Python REPL but I can't do it because of the type system". Casting is indeed a big overhead if you're doing it everywhere, but my experience is the cases where you need it are extremely rare.

amelius 10y ago

> A type is a collection of possible values Ok, but do two collections with the same values always correspond to the same type?

kd0amg 10y ago
It depends on the language. If you have, for example, a type-and-effect system, a type can contain information (like "we wrote to stdout while computing this") that is never reflected in the value itself. In a formal setting, it's more appropriate to describe a type as a collection of pieces of source code, so that `2+3` and `print "computing...\n"; 2+3` have different types even though they'll evaluate to the same thing.
paulddraper 10y ago
Yes, but if remember you can always say that the values are different. A blue 5, and a red 5. Five feet, or five inches.
munificent 10y ago
Yes, they do.
acjohnson55 10y ago
Generally, no, at least with nominal typing.

naasking 10y ago

Decent overview of many concepts, but the opening line isn't strictly true: > A type is a collection of possible values. A type is a proposition, and "This binding has one of these possible values" is merely one type of proposition. So a type is much more powerful than a simple set-based interpretation, even though this is how most people think about it. For instance, in Haskell you can encode a region calculus that ensures prompt reclamation of file handles and other scarce resources [1]. The relations between nested regions to ensure correctness seems awkward to interpret as a set, but it's straightforward if you just think of types as a relation. [1] http://okmij.org/ftp/Haskell/regions.html#light-weight http://okmij.org/ftp/Haskell/regions.html#light-weight

chriswarbo 10y ago
Well, there are several ways to think about types, especially regarding this article, which tries to cover static and dynamic types. Most formal definitions/treatments of types I've come across do not apply to dynamic types at all; usually the typing formalism says nothing about dynamically typed programs/values other than giving them one big recursive type. What we would informally call "dynamic types" are then treated completely separately, e.g. via "tags". While such distinctions are certainly useful, an introductory/broad-overview explanation like this seems to benefit without such complications/distractions.
- naasking 10y ago
  > While such distinctions are certainly useful, an introductory/broad-overview explanation like this seems to benefit without such complications/distractions. I don't think misrepresenting types is the way to go. An introduction like I just gave seems simple enough, where a type is a proposition about a program, and you just then explain that most such propositions are "variable X may take on values from set Y". It's important not to perpetuate the false notion that sets of simple sets of values suffice to explain types, because it entails the common and equally false notion that full test coverage in a dynamically typed language suffices to match the safety of a statically typed language.
  - 10y ago

levbrie 10y ago

Kind of shocked nobody mentioned this, even if it is a bit of an aside, but umm, I've been dying for anything at all from Gary Bernhardt - I don't even know what to say except that it makes me hope however unrealistically that will one day get something like the magnum opus that is "Destroy All Software" from him again.

dochtman 10y ago
You know he just started to post new stuff, right? https://www.destroyallsoftware.com/screencasts/catalog https://www.destroyallsoftware.com/screencasts/catalog
- deleted 10y ago
  [deleted]
- levbrie 10y ago
  I know. Mind blown.
nickpsecurity 10y ago
I havent read/seen it. Im guessing you know more than Id see in an abstract. So, what's the significance of that work?

athenot 10y ago

I've been very curious about Perl6's gradual typing[1] which, as I understand it, draws a lot from Haskell's type system but in an optional manner. subset NonNegativeInt of Int where * >= 0; sub fib(NonNegativeInt $nth) { given $nth { when 0 { 0 } when 1 { 1 } default { fib($nth-1) + fib($nth-2) } } } [1] http://blogs.perl.org/users/ovid/2015/02/avoid-a-common-software-bug-by-using-perl-6.html http://blogs.perl.org/users/ovid/2015/02/avoid-a-common-soft...

zeveb 10y ago

> The unsatisfying solution used in practice is to give eval() the type Any, which is like Object in some OO languages or interface {} in Go: it's the type that can have any value. Values of type Any aren't constrained in any way, so this effectively removes the type system's ability to help us with code involving eval. Languages with both eval and a type system have to abandon type safety whenever eval is used. It's not quite true that they must abandon type safety: rather, they must abandon a certain kind of compile-time type check. It's not unsafe to use eval or Any values (i.e., it won't crash the system); one must simply examine the Any value (at runtime, natch) and do stuff with it.

eximius 10y ago

So, how do these advanced types work? For their `add` example, I imagine just having x<y somewhere is sufficient. But let's say I write a sorting implementation but the compiler can't quite figure out that it is correct. Is there a provided way to tell the compiler 'trust me, this property is now true'? Also, I'm assuming the compiler has two classes of errors here: a counter example vs. unable to prove? Can anyone point me to documentation on these (in Idris, preferably)?

icen 10y ago
In Idris, there are functions `believe_me` and `really_believe_me`, which assert things to the compiler. They're generally only used for FFI code, or for extremely tedious proofs. If you wanted to prove that a list was sorted, you'd write another datatype: IsSorted : Ord a => List a -> Type which represents the proposition that the input list is sorted. You could encode this by requiring that any new element in the list is either the first element, or less than or equal to the previous element. Then, your sorting function could return a dependent pair: (l : List a ** IsSorted l) which can be read as the list, accompanied by a proof that it is, in fact, sorted. Since your `IsSorted` type requires that the list is sorted, via construction, you won't be able to supply the output of the function unless your code is correct (or you use `believe_me`!). The compiler doesn't generally come up with counterexamples for you; with this style, if the proof isn't complete, it won't compile.

mamcx 10y ago

I read that type checking is easier with dependent types. I'm barely aware of adga adn other langs that are used for profs, but wonder how useful (and what danger ahead) could cause to design a language with this for more mundane purposes (like, for example, build websites, data manipulation, gui, etc)

rpazyaquian 10y ago

What types are and what they do is all well and good, but what I want to know is how they would help me write a larger application. Would it help it be more correct, be written faster, or be more flexible? Does it just help on a line-by-line programming basis, or can it have any ramifications on a higher level like product design?