Alguns comentários soltos

Voltando a estudar e praticar Haskell, o que me fez voltar a ler sobre mônadas. Uma coisa que eu ainda não tinha entendido direito é que, apesar da aparência imperativa da notação usando do, um valor envolto em uma mônada é apenas um valor, não é a execução da ação em si. Algo tem que executar as ações. Minha intenção em estudar mônadas é entender suas relações com sistemas de tipos e efeitos, o que leva a regiões para gerenciamento de memória.

E por falar em Haskell, é interessante ver como DSLs como Fran (ou outras que utilizam a idéia da reatividade funcional) são expressivas e só são possíveis em Haskell. Elas utilizam exatamente o conjunto que distingue a linguagem: avaliação preguiçosa, type classes e mônadas.

Sim, também tenho lido sobre uso de código carregado dinamicamente em uma linguagem com verificação estática de tipos (Haskell, novamente), um interesse antigo pois tem tudo a ver com sistemas distribuídos e código móvel. O hs-plugins faz o possível mas algumas coisas ainda são impossíveis, e talvez menos flexíveis do que deveriam. Por exemplo, uma aplicação que tenha plugins deve definir a priori as interfaces que os plugins devem obedecer, algo similar aos pontos de extensão da plataforma Eclipse. Por que não ter plugins que não necessariamente sigam (ou nao estritamente) a API delimitada pela aplicação? O maior problema é, como verificar os tipos de um plugin arbitrário, o que já é significantemente difícil no cenário com uma interface definida. Uma idéia poderia ser usar proof-carrying code para isso, de fato um uso talvez simplório, mas realizável, da idéia. É uma das coisas que eu espero investigar em breve. E Typed Assembly Language é o futuro.

Pesquisa em linguagens de programação e espeficicações formais

Ainda não veio a inspiração (ou foi a preguiça que não deu trégua) para escrever sobre a correspondência de Church-Turing. Enquanto isso, este post, já antigo, de Erik Meijer em seu blog e os comentários discutem muito bem sobre o uso de definições precisas da semântica de uma linguagem de programação. O ponto mais importante, na minha opinião, está nesse parágrafo de Erik:

Of course the question is why smart language designers do not write formal specifications, and why equally brilliant researchers do not cover the complete design of real languages. The simple, recursive, answer I believe is that despite decades of research (van Wijngaarden grammars, attribute grammars, denotational semantics, operational semantics, axiomatic semantics, VDM, ASF/SDF, theorem provers, abstract state machines, ...........................) we still lack the proper programming language to describe real programming languages at the right level of abstraction.

E é ecoado no comentário de Neel Krishnaswami:

Our formal descriptions don't evolve as quickly as our code, for reasons I don't really understand. Eg, SML has evolved much more slowly than Ocaml or Haskell have, AFAICT because it has a formal semantics and they don't. So when a change is made to Ocaml, the implementors don't feel obligated to redo all of the soundness proofs -- which is good, because the proofs are sufficiently unmodular that even small changes can involve lots of work to fix. (Bob Harper and Chris Stone complain about this problem in so many words in their type-theoretic semantics of SML.)

Por enquanto fiquemos com um pouco de Dó sustenido

Aqui um post que eu escrevi no Googletron sobre as novas características que aparecerão na versão 3 da linguagem C#, que pelo jeito está praticamente se tornando objeto-funcional. I mean, inferência de tipos? Expressões lambda? (Inclusive sem inventar algum nome mais "marketeiro" para substituir "lambda").

Lembrando que C# já tem suporte a polimorfismo paramétrico desde a versão 2... ora, inventem logo uma versão puramente funcional do CLR. Haskell para as massas!

Promessas

Ok, eu tinha ficado de publicar um artigo sobre prova de teoremas na programação aqui, há um bom tempo já. Mas vieram as provas de final de semestre, e vieram as curtas férias, e isso foi ficando para depois. Em breve a atividade no blog deve aumentar, aproveitando que as disciplinas acabaram e eu vou me dedicar mais à pesquisa. E o artigo prometido ainda vai aparecer.