undefined | Better HN

0 pointslmm10y ago0 comments

ML is good at what it does but it doesn't offer Haskell's type system.

I won't comment on history and I see no value in unpleasantness, but I do think that knowing what we know now, and particularly in the light of Idris, the advantages of laziness are overstated and strict languages (or possibly explicit codata) are the future of programming. And if true, that puts Haskell in an awkward position.

0 comments

7 comments · 2 top-level

Drup10y ago· 3 in thread

> ML is good at what it does but it doesn't offer Haskell's type system.

You can do most of Haskell's type trickery in OCaml though. Some things are much easier in Haskell, but other things are much harder.

wyager10y ago

I really don't see how.

There's a ton of useful stuff with HKTs, type families, GADTs, etc that you can't hope to achieve with ocaml's type system.

Recently, I've found myself using extensive type-level arithmetic for automatic hardware generation and verification. This requires a number of powerful type system features (type level literals, kind promotion, type functions and equality constraints a la type families, type normalization plugins) that wouldn't work at all in ocaml.

lmmOP10y ago

Can you? I use higher-kinded types all the time, and OCaml simply doesn't have them AIUI.

Drup10y ago

Most examples of HKT in Haskell are either:

- not necessary. You don't need HKTs to have >>= for your favorite monad.

- encodable in functors/first class modules trivially.

- genuinely complicated HKT.

The last point happens far less often than Haskell people believe. (It does happen occasionally, though, and it's indeed annoying when it does).

1 more reply

Kutta10y ago· 2 in thread

I don't see why Haskell's in an awkward situation. Adding more strictness support to GHC is not particularly hard and it's happening already. It's far easier to add strictness to GHC than to launch a competitor production-strength pure functional language.

(On the long term, probably we'll see a brave new type-theoretical language, when much of the current research crystallizes into something tangible; but until then I don't see GHC being overshadowed by competitors. There is lots of inertia and the extant GHC infrastructure is extremely valuable. Dependent types are very important and adding them to GHC is very hard, but it's still happening, so Idris & co. will have a difficult time trying to fish in that pond)

AnimalMuppet10y ago

Can someone explain to me what exactly dependent types are that Haskell doesn't already have? I thought Haskell already offered dependent types.

lmmOP10y ago

Haskell has some efforts, but IIRC nothing that's as clear and maintainable as just writing a function from types to types like you can do in Idris.

j / k navigate · click thread line to collapse

0 comments

7 comments · 2 top-level

Drup10y ago· 3 in thread

> ML is good at what it does but it doesn't offer Haskell's type system.

You can do most of Haskell's type trickery in OCaml though. Some things are much easier in Haskell, but other things are much harder.

wyager10y ago

I really don't see how.

There's a ton of useful stuff with HKTs, type families, GADTs, etc that you can't hope to achieve with ocaml's type system.

lmmOP10y ago

Can you? I use higher-kinded types all the time, and OCaml simply doesn't have them AIUI.

Drup10y ago

Most examples of HKT in Haskell are either:

- not necessary. You don't need HKTs to have >>= for your favorite monad.

- encodable in functors/first class modules trivially.

- genuinely complicated HKT.

The last point happens far less often than Haskell people believe. (It does happen occasionally, though, and it's indeed annoying when it does).

1 more reply

Kutta10y ago· 2 in thread

AnimalMuppet10y ago

Can someone explain to me what exactly dependent types are that Haskell doesn't already have? I thought Haskell already offered dependent types.

lmmOP10y ago

Haskell has some efforts, but IIRC nothing that's as clear and maintainable as just writing a function from types to types like you can do in Idris.

j / k navigate · click thread line to collapse