[Haskell-cafe] DTP10 Call for Participation

[Conor McBride]

On 6 May 2010, at 16:04, Colin Paul Adams wrote:

>>>>>> "Conor" == Conor McBride <conor at strictlypositive.org> writes:
>
>    Conor> Remember, Haskell is the world's most popular dependently
>    Conor> typed functional programming language...
>
> Could you justify that claim please?

Is that a feature request or a sceptical objection? If the former,
I'm on the case already. If the latter... avec plaisir.

Which part of it do you dispute? That Haskell is a dependently
typed functional programming language? Justification:

   cabal install she

I know. It's not Haskell in the sense that the language compiled
by GHC is not Haskell. The genie is far enough out of the bottle.

Or is it my claim that Haskell is more popular than the other
dependently typed programming languages?

   Judging by community traffic, Haskell is more popular than Coq.
   By construction, Haskell is at least as popular as Agda.
   I could name a few others (e.g., ATS, Idris), but they're clearly
     not touching Haskell for presence.

Now, of course, the dependently typed functionality available in
Haskell is a bit rudimentary compared to functional languages
defined with dependent types in mind. I certainly don't think
Haskell is popular for being dependently typed, or that
dependently typed programmers favour Haskell as weapon-of-choice
(actually, for language *implementation*, many of us do), but I
was careful not to claim either of those things.

Haskell has data-indexed types, via a suitable encoding, which
SHE automates, and even some dependency on run-time data, via
a singleton type encoding (the ugliness of which SHE does her
best to tidy away). Everything you need to start experimenting
with indexing your data and control structures is in the box
already. Indexed versions of Functor and Monad are already
beginning to emerge and prove useful. Indexed Monads are just
what you get when you yank Hoare Logic through the Curry-Howard
correspondence from proof to programming. Key question: how
should the library equip us to exploit these notions effectively?

So I will finish with some bold speculation, as it's election day
and I've constructed enough content-free sloganeering already.
If you want to use a bit of dependent typing pervasively in a real
world application, linking with a wealth of libraries, Haskell's
likely to be your best bet. For now. For a while yet, actually.

Interesting times

Conor