Wnioskowanie typu na podstawie ograniczeń z danymi algebraicznymi

Pracuję nad językiem genealogicznym ML opartym na wyrażeniach, więc oczywiście wymaga wnioskowania typu> :)

Teraz próbuję rozszerzyć oparte na ograniczeniach rozwiązanie problemu wnioskowania typów, oparte na prostej implementacji w EOPL (Friedman i Wand), ale są to eleganckie algebraiczne typy danych.

To, co mam do tej pory, działa płynnie; Jeśli wyrażenie ejest a + b, e : Int, a : Inti b : Int. Jeśli epasuje

match n with
  | 0 -> 1
  | n' -> n' * fac(n - 1)`,

Mogę słusznie wywnioskować, że t(e) = t(the whole match expression), t(n) = t(0) = t(n'), t(match) = t(1) = t(n' * fac(n - 1)i tak dalej ...

Ale jestem bardzo niepewny, jeśli chodzi o algebraiczne typy danych. Załóżmy, że funkcja taka jak filtr:

let filter pred list =
  match list with
    | Empty -> Empty
    | Cons(e, ls') when pred e -> Cons (e, filter ls')
    | Cons(_, ls') -> filter

Aby typ listy pozostał polimorficzny, Cons musi być typu a * a list -> a list. Tak więc, przy ustalaniu tych ograniczeń, to oczywiście trzeba zajrzeć do tych typów moich algebraicznych konstruktorów - problem mam teraz jest „kontekst czułości” wielu zastosowań algebraicznych konstruktorów - jak mogę wyrazić w moim równań więzów, że aw każda sprawa musi być taka sama?

Mam problem ze znalezieniem ogólnego rozwiązania tego problemu i nie jestem w stanie znaleźć na ten temat dużej literatury. Ilekroć znajdę coś podobnego - język oparty na wyrażeniach z wnioskowaniem typu na podstawie ograniczeń - przestają mieć tylko algebraiczne typy danych i polimorfizm.

Wszelkie uwagi są mile widziane!

programming-languages type-theory functional-programming inductive-datatypes typing Kris
źródło

@Guy Nie chcę brzmieć niewdzięcznie, ale nie szukam gotowego rozwiązania - masz jakieś sugestie? Większość istniejących dokumentów, które udało mi się znaleźć (jak dokumenty INRIA na temat ML, OCaml ...) są znacznie obszerniejsze niż to, czego potrzebuję (i jestem w stanie zrozumieć).

Kris,

Zacznę od rozdziału wnioskowania w ATTAPL , myślę, że omawiają wszystko, czego potrzebujesz na dostępnym poziomie.

Gilles 'SO - przestań być zły'

@Gilles Myślę, że ATTAPL jest jedyną „klasyczną” książką PL, której nie mam na półce: P Ale dzięki, przyjrzę się w poniedziałek, siedzę na podłodze w Uni z około 10 egzemplarzami rozrzuconymi po biurach: )

Kris,

@Kris, czy kiedykolwiek znalazłeś dostępny zasób rozwiązujący ten problem? Moja implementacja „mini ML” utknęła właśnie na tym problemie ... Myślę, że znalazłem odpowiedni rozdział z ATTAPL ( pauillac.inria.fr/~fpottier/publis/emlti-final.pdf ) i przejrzałem rozdział o algebraice typy danych, ale obawiam się, że to trochę ponad moją głowę.

michiakig

@spacemanaki Tak, od tego czasu uważam, że pdfs.semanticscholar.org/8983/... jest doskonałym źródłem informacji na ten temat.

Kris,

Wnioskowanie typu na podstawie ograniczeń z danymi algebraicznymi

Odpowiedzi: