4 ms·

Unfortunately I do not know so well Haskell to give you an answer. I was referring to this: > I think this is because there is yet to be a language that makes

by gcanti 12y ago

Unfortunately I do not know so well Haskell to give you an answer. I was referring to this: > I think this is because there is yet to be a language that makes expressing complex types easy. Since I'm obliged to use a dynamic language (JavaScript) I'm looking for a solution in it. And in JavaScript is really easy to express a complex type, say "the set of all the even integers between 2 and 14 but 10", using runtime checking to enforce the constraints. Is it simple in Haskell to define such a set in its type system?

agumonkey 12y ago
I do not know Haskell enough either. But I didn't really mean 'using type system everywhere'. About your question, from what I've seen you can always go symbolic : define an abstract thing as twofourteenexceptten that represent that idea and use it. Or just use a filter everywhere to ensure that function requiring a 2and14but10 won't be called on something with other numbers. In that case you're not losing anything you'd do with a dynamic language.
lmm 12y ago
Simple? Yes. Pleasant? Not really. I'm not a Haskell expert but I can write that type in Scala (the Haskell version probably has less boilerplate, but still some): sealed trait Even[N <: Nat] object Even { implicit object zero extends Even[_0] implicit def evenSS[N <: Nat](implicit e: Even[N]) = new Even[S[S[N]]]{} } sealed trait EvenAndBetweenTwoAndFourteenAndNotTen object EvenAndBetweenTwoAndFourteenAndNotTen { implicit def forN[N <: Nat](implicit e: Even[N], le2: Le[_2, N], le14: Le[N, _14]) = new EvenAndBetweenTwoAndFourteenAndNotTen[N]{} implicit object interfere10 extends EvenAndBetweenTwoAndFourteenAndTen[_10] } Like I said, it's cumbersome, but there's nothing actually complicated about writing this, it's just boilerplate to represent it in the type system. On the other hand, in Idris or the other languages mentioned in the article, you should be able to write that kind of constraint at the type level just as easily as you can at the value level. That's where it gets really exciting.
dragonwriter 12y ago
That's not really expressing a complex type in JavaScript, its expressing a complex (such as it is) runtime constraint -- which you can do easily in Haskell as well. JS doesn't give you anything Haskell doesn't there. Its true that to make that a proper, statically-enforced type in Haskell takes some complexity, but if you aren't willing to do that, you could make it a runtime-enforced constraint on a statically-enforced type of integers as easily in Haskell as, in JavaScript, you could make it a runtime-enforced constraint on a value that is not statically enforced to be anything more specifically than a valid JS value.
sanderjd 12y ago
In javascript, any method that relies on receiving a value of "the set of all the even integers between 2 and 14 but 10" should probably check that it did in fact receive such a thing or it might be buggy. In a statically typed language, that check can easily be centralized to wherever an `EvensFrom2To14Without10` value is constructed. Here's an example in rust[0]. If the `print_bare` method relies on only receiving even numbers between 2 and 14 excluding 10, then it is buggy, because it isn't checking its input, but the `print_tagged` method is correct without needing to check! [0]: http://is.gd/9uHrc7 http://is.gd/9uHrc7

by gcanti 12y ago

agumonkey 12y ago

I do not know Haskell enough either. But I didn't really mean 'using type system everywhere'. About your question, from what I've seen you can always go symbolic : define an abstract thing as twofourteenexceptten that represent that idea and use it. Or just use a filter everywhere to ensure that function requiring a 2and14but10 won't be called on something with other numbers. In that case you're not losing anything you'd do with a dynamic language.

lmm 12y ago

Simple? Yes. Pleasant? Not really. I'm not a Haskell expert but I can write that type in Scala (the Haskell version probably has less boilerplate, but still some): sealed trait Even[N <: Nat] object Even { implicit object zero extends Even[_0] implicit def evenSS[N <: Nat](implicit e: Even[N]) = new Even[S[S[N]]]{} } sealed trait EvenAndBetweenTwoAndFourteenAndNotTen object EvenAndBetweenTwoAndFourteenAndNotTen { implicit def forN[N <: Nat](implicit e: Even[N], le2: Le[_2, N], le14: Le[N, _14]) = new EvenAndBetweenTwoAndFourteenAndNotTen[N]{} implicit object interfere10 extends EvenAndBetweenTwoAndFourteenAndTen[_10] } Like I said, it's cumbersome, but there's nothing actually complicated about writing this, it's just boilerplate to represent it in the type system. On the other hand, in Idris or the other languages mentioned in the article, you should be able to write that kind of constraint at the type level just as easily as you can at the value level. That's where it gets really exciting.

dragonwriter 12y ago

That's not really expressing a complex type in JavaScript, its expressing a complex (such as it is) runtime constraint -- which you can do easily in Haskell as well. JS doesn't give you anything Haskell doesn't there. Its true that to make that a proper, statically-enforced type in Haskell takes some complexity, but if you aren't willing to do that, you could make it a runtime-enforced constraint on a statically-enforced type of integers as easily in Haskell as, in JavaScript, you could make it a runtime-enforced constraint on a value that is not statically enforced to be anything more specifically than a valid JS value.

sanderjd 12y ago

In javascript, any method that relies on receiving a value of "the set of all the even integers between 2 and 14 but 10" should probably check that it did in fact receive such a thing or it might be buggy. In a statically typed language, that check can easily be centralized to wherever an `EvensFrom2To14Without10` value is constructed. Here's an example in rust[0]. If the `print_bare` method relies on only receiving even numbers between 2 and 14 excluding 10, then it is buggy, because it isn't checking its input, but the `print_tagged` method is correct without needing to check! [0]: http://is.gd/9uHrc7 http://is.gd/9uHrc7