Re: [Haskell-cafe] DTP10 Call for Participation

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

...

...

...

...

...

"Conor" == Conor McBride 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