Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Types

gist.github.com

Post reply on HN
Print view View original

21–30 of 198 posts

Re: Types

#21

Post by seanwilson »

continuational wrote: post #16
seanwilson wrote: post #11

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 e…

To some degree, you can choose what you want to prove about your algorithms in those languages. It's perfectly possible to implement a sorting algorithm without proving that it actually sorts the input, or indeed returns a permutation of the input list at all. In that sense, you can choose how much efford you want to put into it.

> To some degree, you can choose what you want to prove about your algorithms in those languages. > It's perfectly possible to implement a sorting algorithm without proving that it actually sorts the input, or indeed returns a permutation of the input list at all.

Sure, but my point is that any nontrivial property requires the programmer to write difficult formal mathematical proofs which is an activity completely unlike what you see in mainstream strongly typed languages (e.g. Haskell, OCaml).

Also, consider how when you start making use of generics in type systems by converting all you Object lists to String lists; you find you have to start adding generic types all over the place for any code that touches that code until the compiler errors stop. If you decided to capture permutations of input lists in a dependently typed language, the exact same thing happens except this time capturing that property for all your algorithms could be monumental task of writing complex proofs (unlike before where you're just labelling things).

Re: Types

#22

Post by catnaroek »

seanwilson wrote: post #11

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 e…

Agreed. These days, the most popular dependently typed languages are based on some variant of Martin-Löf type theory, in which arbitrary mathematical propositions are expressible at the type level. I'm not convinced that these designs offer a good power/cost ratio. For example, these languages often have very limited type inference.

In practice, most of the properties that a programmer (rather than, say, a mathematician using a proof assistant) would want to enforce mechanically (say, invariants of data structures) are expressible as first-order statements (lambda-bound variables are never applied). This strongly suggests that the ergonomics of dependent types could be significantly improved by deliberately limiting their expressive power. By the way, the idea isn't new: the Damas-Milner type system, which is most certainly known and proven technology, is a subset of System F-omega's type system for which type inference is possible, at the reasonable (IMO) price of not having higher-ranked or higher-kinded types. A dependently typed language with a first-order type level would benefit from reusing the basic architecture of a Damas-Milner type checker: a constraint generator and a constraint solver powered by a first-order unification engine.

Re: Types

#23

Post by titanomachy »

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.

Re: Types

#24

Post by epidemian »

NhanH wrote: post #15

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 boun…

> The author is highly probably on the static typing camp.

First and foremost, i don't think dividing people into these clear-cut "camps" is good for this discussion (and probably for most discussions too...).

Second, i very much doubt that the author is a purist of static typing, or even a strong proponent of it. He has a series of programming screencasts called Destroy All Software, and in most the episodes i've seen he uses Ruby, Bash or Python. So, unless he has dramatically changed his style since then, i don't think he has any problems using dynamically typed languages.

Re: Types

#25

Post by NhanH »

epidemian wrote: post #24
NhanH wrote: post #15

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 boun…

> The author is highly probably on the static typing camp. First and foremost, i don't think dividing people into these clear-cut "camps" is good for this discussion (and probably for most discussions too...). Second, i very much doubt that the author is a purist of static typing, or even a strong proponent of it. He has a series of programming screencasts called Destroy All Software, and in most the episodes i've se…

Sure, I will edit that sentence out.

Re: Types

#26

Post by seanwilson »

catnaroek wrote: post #22
seanwilson wrote: post #11

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 e…

Agreed. These days, the most popular dependently typed languages are based on some variant of Martin-Löf type theory, in which arbitrary mathematical propositions are expressible at the type level. I'm not convinced that these designs offer a good power/cost ratio. For example, these languages often have very limited type inference. In practice, most of the properties that a programmer (rather than, say, a mathematic…

> By the way, the idea of deliberately limiting the expressive power of types isn't new: the Damas-Milner type system, which is most certainly known and proven technology, is a first-order subset of System F-omega's type system for which type inference is possible. A dependently typed language with a first-order type level would benefit from reusing the basic architecture of a Damas-Milner type checker: a constraint generator and a constraint solver powered by a first-order unification engine.

Have you seen languages like DML (let's you capture linear arithmetic properties only and automates the proof of these)?

https://www.cs.bu.edu/~hwxi/DML/DML.html

> Dependent ML (DML) is a conservative extension of the functional programming language ML. The type system of DML enriches that of ML with a restricted form of dependent types. This allows many interesting program properties such as memory safety and termination to be captured in the type system of DML and then be verified at compiler-time.

What program properties are useful to capture and what properties you can mostly automate is a really interesting problem.

Re: Types

#27

Post by catnaroek »

seanwilson wrote: post #26
catnaroek wrote: post #22

Earlier quoted context omitted.

Agreed. These days, the most popular dependently typed languages are based on some variant of Martin-Löf type theory, in which arbitrary mathematical propositions are expressible at the type level. I'm not convinced that these designs offer a good power/cost ratio. For example, these languages often have very limited type inference. In practice, most of the properties that a programmer (rather than, say, a mathematic…

> By the way, the idea of deliberately limiting the expressive power of types isn't new: the Damas-Milner type system, which is most certainly known and proven technology, is a first-order subset of System F-omega's type system for which type inference is possible. A dependently typed language with a first-order type level would benefit from reusing the basic architecture of a Damas-Milner type checker: a constraint…

> Have you seen languages like DML (let's you capture linear arithmetic properties only and automates the proof of these)?

Yes. But what I have in mind is a little bit more ambitious. I want dependent types restricted to be parameterized by syntactic values (in the sense of ML's value restriction) of what Standard ML calls `eqtype`s. For example, correctly balanced red-black trees would be:

    (* clearly eqtypes *)
    datatype Color = R' | B'
    datatype Nat = Z | S : Nat -> Nat
    
    datatype Tree =
      | Empty : Tree (B', Z, 'a)
      | R : Tree (B', 'h, 'a) * 'a * Tree (B', 'h, 'a) -> Tree (R', 'h, 'a)
      | B : Tree ('c, 'h, 'a) * 'a * Tree ('c, 'h, 'a) -> Tree (B', S 'h, 'a)

Re: Types

#28

Post by twblalock »

seanwilson wrote: post #17
twblalock wrote: post #13

Earlier quoted context omitted.

What would happen if you did not compare them before calling the function, and just passed them in such that x >= y?

> What would happen if you did not compare them before calling the function, and just passed them in such that x >= y? It would be a type error. All the compiler would know is that "x" and "y" are strings/integers so it would tell you they were the wrong type. If you do a branch on checking they are the correct type, then in that part of the branch the compiler will know they are the correct type and allow "add" to b…

Assuming they were integers before, what type would they become after they were compared?

Re: Types

#29

Post by seanwilson »

titanomachy wrote: post #23

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 co…

> 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!

Re: Types

#30

Post by DSMan195276 »

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.

Post reply on HN