Czy typy własne powodują, że rachunek konstrukcji indukcyjnych staje się przestarzały?

10

Typy własne są rozszerzeniem Rachunku konstrukcji [1], które pozwalają językowi wyrażać algebraiczne typy danych zakodowane za pomocą kodowania Scott. Kodowanie Scott daje możliwość dopasowania do wzorca O(1), który jest jednym z głównych czynników motywujących do włączenia definicji indukcyjnych do CC. Jednak typy własne tworzą znacznie prostszą i elegancką teorię podstawową i wydają się nie mniej potężne.

Czy typy własne, z teoretycznego punktu widzenia, powodują, że CIC staje się przestarzałe, czy też jest jeszcze jakiś aspekt, w którym CIC jest korzystny w stosunku do Self Tyes?

[1] http://staff.computing.dundee.ac.uk/pengfu/document/talks/mvd-2012.pdf

lambda-calculus type-theory functional-programming inductive-datatypes MaiaVictor
źródło
2
Może coś mi brakuje, ale dlaczego autopisy nie są tylko typami rekurencyjnymi (np. Niesłyszalnymi?) Nie jest to celem wszystkich zależnie wpisywanych rzeczy, ale na pewno jest ważne, aby CiC brzmiał. Połączona prezentacja ma również typ pisma, ale nie sądzę, że jest to powiązane / konieczne.
Daniel Gratzer
@ jozefg Rzeczywiście: „Logika będzie niespójna, ale dla programów nie będzie problemu”. Powinieneś opublikować to jako odpowiedź.
Gilles 'SO - przestań być zły'
Czy ten komentarz nie jest skierowany do * : *@GIlles, czy nie Self?
MaiaVictor,
@srvm z napisanymi przez nich regułami pisania są obojętne. Czy masz link do gazety?
Daniel Gratzer
@ jozefg Podejrzewam, że to ten: staff.computing.dundee.ac.uk/pengfu/document/papers/…
gallais

Odpowiedzi:

5

Nie jestem ekspertem w tej pracy, ale wydaje mi się, że głównym bieżącym problemem jest brak dowodu SN, nawet z ograniczeniami. Te dowody są jednak bardzo trudne, nawet jeśli rachunek jest poprawny, więc dałbym mu trochę czasu. Praca jest z pewnością bardzo obiecująca.

Należy zauważyć, że ograniczenia te są w rzeczywistości dość trywialne do wyrażenia, co stanowi dużą część złożoności formułowania rodzin indukcyjnych w CIC. Prawdziwą zaletą takiego podejścia byłoby zwięzłe sformułowanie tych warunków.

Od dawna otwartym problemem jest posiadanie języka zależnego od typu

  • Spójny / normalizujący
  • Potrafi wyrazić wszystkie rodziny typów z Coq (a nawet Agda)
  • Pozwala na proste wyrażenie rekurencji w tych rodzinach
  • Prosty lub ma niewielką liczbę podstawowych konstrukcji ( ).Π,Σ,μ

Jedną z takich prób, o których wiem, jest język Altenkirch i al , który podobnie nie ma pełnego studium metaoretycznego (i również nie jest spójny bez dalszych ograniczeń).ΠΣ

cody
źródło