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

Make the Type System Do the Work

nathan.ca

Post reply on HN
Print view View original

121–130 of 141 posts

Re: Make the Type System Do the Work

#121

Post by platz »

moron4hire wrote: post #119
platz wrote: post #117

Earlier quoted context omitted.

Interesting problem! I was wondering why even define things like SquareMeters, but as you say the issues is reducing the terms that have different forms but mean the same thing.

Having a SquareMeters type was meant to reduce complexity. Instead of always dealing with Area all the time, it was meant to be a shortcut. Hrm, what about namespace aliasing? "using SquareMeters = Composite "? Since the problem is not the composition of the type but the verbosity of the deeply composited types, then perhaps it's just about making a shortcut for the name.

things can be composed different ways. m/s^2 should equal (m/s)/s

Re: Make the Type System Do the Work

#122

Post by skybrian »

herge wrote: post #112
skybrian wrote: post #16

This is a good trick but it needs to be used judiciously or you'll end up with lots of boilerplate. I particularly like Go's type system, though, because it makes it very simple: type celsius float64 There's no overhead and it doesn't attempt to prevent you from doing any calculations as a float64; the type checking just prevents direct assignments from a celsius type to another type.

I got annoyed with Go when I learnt how hard it is to sort arbitrary lists. Doing the following in Go is quite a pain: scores = [{'name': 'Bob', 'score': 20}, {'name': 'Jane', 'score': 15}] scores.sort(key=lambda x: x['score'])

Yes, there is in practice a fair bit of boilerplate in Go. (The way you'd do it in this case is by defining two new types for a struct and a slice of structs. Not that hard once you know the trick.)

Still, they got tiny types right, and without getting bogged down in dimensional analysis.

Re: Make the Type System Do the Work

#123

Post by mcguire »

zvrba wrote: post #76
jeffdavis wrote: post #51

"'Dog is-a Mammal' ... actually fairly sound" I disagree in the context of OOP inheritance. (This example uses shapes, because the idea of mutating mammals gets a little strange.) Let's say you have a Circle class and an Ellipse class. A Circle inherits from an Ellipse, of course, because a Circle is-a Ellipse. By specializing as a Circle, we get extra reader methods such as getRadius(). Great. But what about mutator…

The circle vs ellipse problem is rather artificial and, if anything, it shows that modeling with types and everyday intuition are two different things. If the rest of your program can handle general ellipses, it should also be able to handle ellipses having the same minor and major radius (i.e., circles). The obvious solution is to not have the Circle class and _maybe_ equip Ellipse with IsCircle() method. (Though, w…

Weirdly, the C++ Faq taught me more about object-oriented and related issues than any other source. It's very good.

Re: Make the Type System Do the Work

#124

Post by mcguire »

tel wrote: post #35
Buttons840 wrote: post #18

Earlier quoted context omitted.

What are your impressions of the three languages? Personally, I'm learning Haskell first, because Haskell is the most popular of the three and there is plenty of good learning material. As far as Adga and Idris go, I think Idris looks more appealing.

Learn Haskell first. When you've gotten your head at least partially around it then the latter two become much more approachable. Programming in a dependently typed language is not simple if you're not used to the algebraic methods they're based on. That said, Idris seems to be aiming to be much more "practical" than Agda. Also, all that said, once you start getting to the point where you're really getting comfortabl…

Care to make any comparison to ATS? I have been playing with it a bit lately and having a good time.

Re: Make the Type System Do the Work

#125

Post by pjmlp »

drbawb wrote: post #120
pjmlp wrote: post #73

Earlier quoted context omitted.

> Definitely takes away all the boilerplate. Until you need to write generic code. Then it is casts everywhere and boilerplate to satisfy interfaces.

>... and boilerplate to satisfy the interfaces. Go actually provides facilities for embedding types which helps remove some of the unnecessary boilerplate from satisfying an interface.[1] Through embedding you can leverage the implementation of an existing type to satisfy an interface w/o writing methods to dispatch to that underlying type. [1]: http://golang.org/doc/effective_go.html#embedding

I used Go quite a lot until version 1.0 got released.

You are not explaining nothing new to me.

Re: Make the Type System Do the Work

#126

Post by tel »

mcguire wrote: post #124
tel wrote: post #35

Earlier quoted context omitted.

Learn Haskell first. When you've gotten your head at least partially around it then the latter two become much more approachable. Programming in a dependently typed language is not simple if you're not used to the algebraic methods they're based on. That said, Idris seems to be aiming to be much more "practical" than Agda. Also, all that said, once you start getting to the point where you're really getting comfortabl…

Care to make any comparison to ATS? I have been playing with it a bit lately and having a good time.

I haven't used ATS. My understanding is that it's a dependently systems language which makes me think it'll provide good region types and things like what Rust is trying to offer. In that way I'd say it still differs a lot from, say, Agda, where you're likely to encounter fairly heady questions about equality and algebra very quickly.

But again, I've not used it so I can't much say for certain.

Re: Make the Type System Do the Work

#127

Post by eropple »

yareally wrote: post #78
gizmo686 wrote: post #54

Earlier quoted context omitted.

Would it be possible to do this as a type-alias type thing that disapears at compile time? As far as I am aware, Java has no support for such type aliasing, but it should be possible to add a pre-compiler phase to your build process that replaces these types with what they are aliases of. The only part of this that seems complicated is the type checker, which would need to be aware of the difference between AccountId…

I could see it being done with annotations + processing them perhaps, as some frameworks do for database properties such as index/uniqueness. An object for every scalar datatype is just overkill, even if it solves a legitimate problem.

You could make it a pre-compile step in Maven, maybe. But it'd be gross.

Re: Make the Type System Do the Work

#128

Post by moron4hire »

platz wrote: post #121
moron4hire wrote: post #119

Earlier quoted context omitted.

Having a SquareMeters type was meant to reduce complexity. Instead of always dealing with Area all the time, it was meant to be a shortcut. Hrm, what about namespace aliasing? "using SquareMeters = Composite "? Since the problem is not the composition of the type but the verbosity of the deeply composited types, then perhaps it's just about making a shortcut for the name.

things can be composed different ways. m/s^2 should equal (m/s)/s

Okay, I've definitely convinced myself there is no good way to do this without having to write way too much code over and over again. The problem is basically equivalent to inserting items into a sorted list, but you only have one operation in which to do it. So, you are either limited to simple types, or your code for operations on types explodes trying to define all of the ways to compare types (in a generic sense) and different scenarios for combinations of types.

This requires a Turing-complete type system.

Re: Make the Type System Do the Work

#129

Post by taeric »

tel wrote: post #105
taeric wrote: post #103

Earlier quoted context omitted.

I don't think you really wrote anything I did not acknowledge. Yes, types are a form of complete test over the shape/type of data that they encode. If you can encode your data with the correct type, it will go a long way to making sure you don't have errors in the types. However, I take issue with this statement: "For statically typed languages, the type check is a type of test that just so happens to be very succinc…

The true quicksort example you linked has very little to do with Haskell's type system and everything to do with purity. The qsort version at the bottom of that page is also pretty close to the version used in any mutable language, just with a bit more noise in the syntax. A direct translation to Python might make the syntax easier to understand, though it should be stated that this is not supposed to be pretty Pytho…

My point is pretty much about the "a bit more noise in the syntax." And qsort will only work on array types, something that is typically shunned by people trying to "do all of the work with the type system." Consider the types for "NonEmptyList" and such.

Is it neat when these work? Certainly. Do I think they pay obvious dividends in the effort increase? Not so much. I am open to the argument, but I have yet to see anything compelling. And with so much traction in other areas, I am doubtful that it is anything close to the silver bullet that advocates make it out to be.

Post reply on HN