2013-03-28 16 views
10

Istnieje wiele informacji na temat typów zależnych w Haskell i Scala. Dla OCaml, nie tak bardzo. Czy ktoś jest na tyle kompetentny, aby podać kodowy przykład, jak to osiągnąć w OCaml (jeśli w ogóle jest to możliwe)? Jest oczywiście (porzucony) Dependent ML, ale wydaje się, że nie można włączyć takich rzeczy do "zwykłego" kodu OCaml.Typy zależne w OCaml

Zasadniczo chcę usunąć kod taki jak assert(n > 0) i sprawdzić go podczas kompilacji.

EDIT

Na marginesie, warto wspomnieć o OCaml Hybrid Contract Checking oddział, który mógłby wypełnić niektóre z potrzebami utrzymaniu systemu typu. Zamiast assert(n > 0) byś następnie napisać umowę:

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

Czy mogę zapytać, gdzie jest ta "mnogość informacji na temat typów zależnych w Haskell i Scala"? Pomimo rozsądnego przeglądu społeczności Haskell, nie wiem, do czego się odnosisz. (Zdecydowanie uważam, że praca UPenn nad [Dependently-Typed Haskell] (http://www.cis.upenn.edu/~sweirich/) jest istotna, ale to jest bardzo badawcze, a nie praktyczne, i może nie "dużo" w objętości). Nie mam pojęcia, co myślisz o Scali - może poza relacją z typami zależnymi od ścieżki? – gasche

+0

Ehm, na stackoverflow, myślałem. Może zostałem oszukany przez typy zależne od Scalasa. –

Odpowiedz

10

Odwołanie jest Olega lightweight dependent typing stron z przykładami (w SML lub które można przetłumaczyć na SML) technik zależnych, jak stosowane w językach ml. Jego artykuł na temat Lighweight static capabilities (PDF) z Chung-chieh Shan w 2007 roku jest szczególnie istotny.

Edytuj: Od wersji 4.00 (wydany po napisaniu powyższego dokumentu), OCaml ma GADT, które pozwalają usprawnić kilka technik dla wyrafinowanych informacji statycznych (wcześniej polegających na technikach fantomowych), w szczególności "typach singletonowych" wzór przedstawiony w Omega. Wykazano, że nie są one niezbędne do uzyskania silnego programowania czcionek, ale nadal mogą być wykorzystywane przez różnorodne przykłady znalezione w środowisku naturalnym.