2011-04-06 4 views
10

J'essaie actuellement de déterminer quels aspects de mon programme peuvent être vérifiés statiquement par le compilateur scala. Après avoir lu this question je suis venu avec l'idée de modèles de conception pour les types. Je trouve assez compliqué de comprendre ce qui pourrait être possible avec le système de types de Scala. Donc, je voudrais regarder les usages pratiques (pas l'arithmétique peano ou des trucs comme ça). Des motifs simples qui réapparaissent souvent dans le code normal.Modèles de conception pour la vérification de type statique

Quelqu'un sait-il des blogs ou même des livres qui traitent de cette question? De préférence dans Scala, mais il pourrait aussi être utile pour d'autres langues.

+0

Pourquoi est-ce marqué Haskell? Ces liens peuvent être intéressants: http://blog.ezyang.com/2010/08/type-kata-controlled-sharing-of-references/ et http://blog.ezyang.com/2010/08/type- kata-newtypes/ –

+0

@Edward Parce que le système de type de Scala semble être similaire au système de type de Haskell et peut-être des modèles pour Haskell (qui existe depuis plus longtemps) transférer à Java. – ziggystar

+0

@Edward Je pense que cela est valable parce que les expériences les plus aventureuses avec le système de type de Scala semblent provenir de personnes avec un fond de Haskell, par ex. Le blog de Rúnar et le peuple Scalaz. –

Répondre

6

Je pense que l'une des choses les plus utiles qui mériteraient le nom de "motif de conception" est la technique des "types fantômes". C'est un moyen plus ou moins systématique de coder des informations statiques dans un paramètre de type. Voir quelques exemples:

Vous pourriez également être intéressé par un Oleg wondertrick lié: Lightweight static capabilities (avec Shan Chung-chieh).

+1

[types fantômes dans Scala] (http://james-iry.blogspot.com /2010/10/phantom-types-in-haskell-and-scala.html) – ziggystar

2

Vous pouvez regarder the design advice for Haskell, et plus précisément, quelques-uns des plus des documents de recherche récents sur l'intégration de fortes propriétés dans le système de type:

  • Mettre Curry-Howard au travail Tim Sheard, Proceedings of the ACM 2005 Atelier SIGPLAN sur Haskell. Tallinn, Estonie, 74 - 85, 2005
  • Vérification de programme basée sur le langage par types expressifs Martin Sulzmann et Razvan Voicu. En langage de programmation conforme à la vérification du programme (PLPV'06)
  • Contrats dactylographiés pour la programmation fonctionnelle Ralf Hinze, Johan Jeuring et Andres Loh.
  • Une bibliothèque pour la sécurité des flux d'informations légères dans Haskell A Russo, K. Claessen, J. Hughes.

Il n'existe pas encore de méthodologie standard, bien qu'il existe de nombreux exemples de problèmes individuels.

Questions connexes