Czytałem artykuł badawczy o Haskell i sposobie implementacji HList i zastanawiając się, kiedy opisane techniki są i nie są rozstrzygalne dla sprawdzania typu. Ponadto, ponieważ możesz robić podobne rzeczy z GADTs, zastanawiałem się, czy sprawdzanie typu GADT jest zawsze rozstrzygalne.Fundeps i GADTs: Kiedy sprawdzanie typu jest rozstrzygalne?
Wolałbym cytaty, jeśli je masz, abym przeczytał/zrozumiał wyjaśnienia.
Dzięki!
Uważam, że kontrola typu GADT jest zawsze rozstrzygająca; to wnioskowanie jest nierozstrzygalne, ponieważ wymaga unifikacji wyższego rzędu. Ale sprawdzanie typu GADT jest ograniczoną formą sprawdzania dowodów, którą widzisz na przykład. Coq, gdzie konstruktorzy budują okres próbny. Na przykład klasyczny przykład osadzania rachunku lambda w GADTs ma konstruktor dla każdej reguły redukcji, więc jeśli chcesz znaleźć normalną formę terminu, musisz powiedzieć mu, którzy konstruktorzy cię do tego doprowadzą. Problem zatrzymania został przeniesiony w ręce użytkownika :-)
To dobra uwaga. Sądzę więc, że interesuje mnie to, kiedy GHC wnioskuje o GADTs. –
Prawdopodobnie już to zauważyłeś, ale w dziale badań firmy Microsoft znajduje się zbiór artykułów: Type Checking papers. Pierwszy z nich opisuje algorytm rozstrzygający, który faktycznie był stosowany w kompilatorze Haskella.
Wymienione artykuły są dobrymi publikacjami, ale nie wydają się odpowiadać na moje pytanie. –
To pytanie może być lepiej skierowane do autorów pracy badawczej. To trochę ezoteryczne dla Stack Overflow. (Zawsze miałem wielki sukces kontaktując się z badaczami w celu komentowania, zwykle są zachwyceni * każdy * czyta ich pracę.) –
Myślę, że takie podejście (że pytania teoretyczne nie mają wpływu na pragmatyczne forum) jest szkodliwe i przestarzałe. Podejścia pragmatyczne powinny być otwarte na nowe technologie, ponieważ te technologie prawdopodobnie poprawią codzienne działania w najbliższej przyszłości. np: funkcje funkcjonalne w języku C#/python. – rcreswick
To powiedziawszy, komentarz Chirsa jest prawdopodobnie prawy, praktycznie rzecz biorąc. Chciałbym, żeby tak nie było. – rcreswick