Haskell, guarantees and pusillanimity

[pozorvlak]

Many times in the course of my Haskell apprenticeship, I've had conversations of the following form:

Me: I want to do X in Haskell, but the obvious thing doesn't work. How do I do it?
Sensei (usually Duncan or totherme): Oh no, you can't do that! If you could do that, then you could have a transperambic Papadopolous twisted asiatic sine-curve

Comments

[beelsebob]

I think really you've hit the "use the right language for the job" barrier. I've been using Haskell for all my code for many years now, and never once hit a need to use any form of fancy type system (hey my code compiles in nhc for gods sake)... For my purposes, Haskell provides me with really tight guarentees and enough expressivity. For you it seems it doesn't provide enough expressivity, my suggestion is use a language that does. In fact, my suggestion is use the language that provides the most guarentees for your required level of expressivity. This is why I am a Haskell programmer.

Bob

[pozorvlak]

I dunno... maybe it's because I'm doing mostly mathematical stuff (the integer-parametrized types problem originally arose while I was writing code for manipulating polynomials over finite fields), maybe it's because I'm coming from a highly dynamic language (Perl) or maybe it's just the kind of person I am, but I seem to run up against some problem of this sort almost every time I pick up a Haskell compiler :-) It could also be because I'm still at the stage of playing with the language and hence keep trying to poke it in funny ways to see what it does...

[beelsebob]

Strange -- I seem to do some fairly similar things, in fact I wrote some code to manipulate polynomials a few weeks ago and didn't hit any problems at all, on the other hand, I'm quite possibly not doing things as complex as you. What representation are you using for your polynomials?

I don't know what you need to use IPTs for, but as far as I've seen IPTs and DTs tend to be used to make type constraints tighter rather than making the type system more expressive. Can you explain the particular problem you need them for?

Bob

[pozorvlak]

The polynomials concerned had coefficients in finite fields, ie all arithmetic was modulo some prime p. I took the view that it didn't make much sense to add (3 mod 7) to (5 mod 11), and wanted the type system to handle that bit for me. I wasn't doing anything particularly complicated other than that.

I want to have a go at it using the library greg_buchholz linked to now :-)

[greg_buchholz]

I took the view that it didn't make much sense to add (3 mod 7) to (5 mod 11), and wanted the type system to handle that bit for me.

In that case you might also like: Implicit configurations -- or, type classes reflect the values of types (Section 3). And if you are new to computing with types in Haskell, I'd suggest Fun with Functional Dependencies or Types as Values in Static Computations in Haskell to get you started.

Types

[cgibbard]

Types are things which will be checked at compile time. You're saying that you're coming from a language like Perl which is mostly untyped (okay, dynamically typed) -- so you ought to be used to not using types to get those compile time guarantees. If some aspect of the type system doesn't seem expressive enough to you, you can usually just not express those things as types. For instance, use an integer at the value, rather than the type level, and turn the thing into a runtime error rather than a compile time one. Sure, it's not as good, but in dynamically typed languages, you generally don't have those compile-time guarantees at all. Take them where you can get them, and if they're really getting in the way, then do things at the value level and avoid the type system.

Of course, it's been pointed out that you really can get integers at the type level, and do all sorts of interesting prolog-esque programming too. For more on that, I recommend looking at HList and OOHaskell, both of which abuse multiparameter typeclasses and

Re: Types

[pozorvlak]

Hello again! :-)

I need to think a bit about how to reply to this, but I wanted to say thanks - that's a really informative response, and I look forward to checking out those links. "try[ing] to allow fancy types in ways that allow the fanciness to be completely localised -- that is, you have additional explicit type signatures only on those values whose types are fancy" sounds like the best solution - if you're doing serious type hackery you probably won't mind too much about having to put the odd type signature in.

Have you read Alexandrescu's Modern C++ Design? It's about some of the extremely cool things you can do with template metaprogramming - dimension checking of physical units, compile-time assertions, all sorts. Highly recommended.

Re: Types

[pozorvlak]

For instance, use an integer at the value, rather than the type level, and turn the thing into a runtime error rather than a compile time one.
Sure, and if I'd been writing in Perl, I would have done exactly that (or just not bothered, and relied on myself to either not write code that added incompatible things, or detect it in testing). But as I was writing in Haskell, and had the World's Most Advanced Type System (TM) around, and the constraints I was dealing with were clearly type-like, it was rather annoying that I couldn't express them using the type system :-) I think in the end I wrote a Perl script to generate the code for each integer I needed (this was before I learned Template Haskell). Then I graduated, got a job, and lost interest for a while.