2013-03-28 13 views
10

Es gibt viele Informationen über abhängige Typen in Haskell und Scala. Für OCaml, nicht so sehr. Ist jemand in der Lage, ein Coding-Beispiel dafür zu liefern, wie dies in OCaml zu erreichen ist (wenn es überhaupt möglich ist)? Es gibt natürlich (die aufgegebenen) Dependent ML, aber es scheint nicht möglich, solche Sachen in "normalen" OCaml-Code einzubauen.Abhängige Typen in OCaml

Grundsätzlich, was ich tun möchte, ist Code wie assert(n > 0) zu entfernen und überprüfen Sie es bei der Kompilierung.

EDIT

Als Randbemerkung, es lohnt sich, die OCaml Hybrid Contract Checking Zweig zu erwähnen, das könnte einige der Bedürfnisse eines abhängigen Typsystem füllen. Statt assert(n > 0) würden Sie dann einen Vertrag schreiben:

contract f = {x : x > 0} -> int 
let f x = x + 1 
let dummy_variable = f (-1) (* Won't compile *) 
+2

Darf ich fragen, wo ist das "viele Informationen über abhängige Typen in Haskell und Scala"? Trotz eines vernünftigen Überblicks über die Haskell-Community weiß ich nicht, worauf Sie sich beziehen. (Ich würde die Arbeit von UPenn an [Dependently-typed Haskell] (http://www.cis.upenn.edu/~sweirich/) als relevant betrachten, aber das ist extrem forschend und nicht praktisch, und vielleicht auch nicht "viel" in Volumen). Ich habe keine Ahnung, was Sie für Scala denken - außer vielleicht die Beziehung zu pfadabhängigen Typen? – gasche

+0

Ehm, auf stackoverflow, dachte ich. Vielleicht wurde ich von Scalas wegabhängigen Typen getäuscht. –

Antwort

10

Ein Referenz Link ist lightweight dependent typing Seiten Oleg, mit Beispielen (in OCaml oder die Sie OCaml übersetzen kann) abhängiger artigen Techniken in ML Sprachen. Seine Arbeit an Lighweight static capabilities (PDF) mit Chung-chieh Shan im Jahr 2007 ist besonders relevant.

Edit: Seit der Version 4.00 (freigegeben, nachdem das Dokument oben geschrieben wurde), OCaml hat GADTs, die einige Techniken für raffinierte statische Informationen straffen lassen (zuvor unter Berufung auf Techniken Phantom-Typs), insbesondere die „Singleton Typen“ Muster gezeigt in Omega. Es wurde gezeigt, dass sie nicht unbedingt notwendig sind, um eine starke typvolle Programmierung zu erhalten, aber sie können immer noch von einer Vielzahl von Beispielen verwendet werden, die in der Wildnis vorkommen.