Pytania otagowane jako type-systems

3
Klasy typów a interfejsy obiektowe
Nie sądzę, że rozumiem klasy typów. Czytałem gdzieś, że myślenie o klasach typów jako „interfejsach” (od OO), które implementuje typ, jest błędne i wprowadza w błąd. Problem polega na tym, że mam problem z postrzeganiem ich jako czegoś innego i jak to jest złe. Na przykład, jeśli mam klasę typu …
2
Jak zdobyć Rachunek Konstrukcji z innych punktów w Kostce Lambda?
CoC jest zwieńczeniem wszystkich trzech wymiarów Lambda Cube. To wcale nie jest dla mnie oczywiste. Wydaje mi się, że rozumiem poszczególne wymiary, a połączenie dowolnych dwóch wydaje się skutkować względnie prostym zjednoczeniem (może czegoś mi brakuje?). Ale kiedy patrzę na CoC, zamiast wyglądać jak połączenie wszystkich trzech, wygląda to zupełnie …
2
Jakie części teorii typów homotopii nie są możliwe w Agdzie lub Coq?
Kiedy patrzymy na książkę, teoria typów homotopii - widzimy następujące tematy: Homotopy type theory 2.1 Types are higher groupoids 2.2 Functions are functors 2.3 Type families are fibrations 2.4 Homotopies and equivalences 2.5 The higher groupoid structure of type formers 2.6 Cartesian product types 2.7 S-types 2.8 The unit type …
4
Jedność parametryczna a parametryczność binarna
Ostatnio zainteresowałem się parametrownością po obejrzeniu artykułu LICS Bernardy'ego i Moulina z 2012 r. ( Https://dl.acm.org/citation.cfm?id=2359499 ). W tym artykule internalizują one jednoargumentową parametryczność w systemie czystego typu z typami zależnymi i podpowiadają, w jaki sposób można rozszerzyć konstrukcję na dowolne arie. Wcześniej widziałem tylko parametr binarny. Moje pytanie brzmi: …
1
Matematyczny (kategoryczny) opis klas typów
Język funkcjonalny można postrzegać jako kategorię, w której jego obiektami są typy, a między nimi funkcjonują morfizmy. Jak pasują klasy w tym modelu? Zakładam, że powinniśmy brać pod uwagę tylko te implementacje, które spełniają ograniczenie większości klas typów, ale które nie są wyrażone w języku Haskell. Na przykład powinniśmy brać …
2
Czy kompilator dla typu zależnego jest znacznie trudniejszy niż interpreter?
Nauczyłem się czegoś o implementowaniu typów zależnych, takich jak ten samouczek , ale większość z nich to implementacja tłumaczy. Moje pytanie brzmi: wydaje się, że implementacja kompilatora dla typu zależnego jest znacznie trudniejsza niż kompilator, ponieważ naprawdę można ocenić argumenty typu zależnego dla sprawdzania typu. Więc Czy moje naiwne wrażenie …
1
Typy zależne od typu kodowanego przez Kościół w PTS / CoC
Eksperymentuję z systemami czystego typu w sześcianie lambda Barendregta, a konkretnie z najsilniejszym z nich, Rachunkiem Konstrukcji. Ten system ma rodzaje *i BOX. Dla przypomnienia, poniżej używam konkretnej składni Mortenarzędzia https://github.com/Gabriel439/Haskell-Morte-Library, która jest zbliżona do klasycznego rachunku lambda. Widzę, że możemy emulować typy indukcyjne za pomocą pewnego rodzaju kodowania podobnego …
3
System typów oparty na naiwnej teorii mnogości
Jak rozumiem, w informatyce typy danych nie są oparte na teorii zbiorów z powodu takich rzeczy jak paradoks Russella, ale tak jak w prawdziwych językach programowania nie możemy wyrazić tak złożonych typów danych jak „zestaw, który nie zawiera siebie”, czy możemy powiedzmy, że w praktyce typ jest nieskończonym zbiorem jego …
2
Intuicja za ścisłą pozytywnością?
Zastanawiam się, czy ktoś może dać mi intuicję, dlaczego ścisła pozytywność indukcyjnych typów danych gwarantuje silną normalizację. Dla jasności widzę, jak negatywne zdarzenia prowadzą do rozbieżności, tj. Poprzez zdefiniowanie: data X where Intro : (X->X) -> X możemy napisać rozbieżną funkcję. Zastanawiam się jednak, jak możemy udowodnić, że ściśle pozytywne …
1
Czy `sort 'można pisać na elementarnej logice afinicznej?
Następujący termin λ, tutaj w formie normalnej: sort = (λabc.(a(λdefg.(f(d(λhij.(j(λkl.(k(λmn.(mhi))l)) (h(λkl.l)i)))(λhi.(i(λjk.(bd(jhk)))(bd(h(λjk.(j (λlm.m)k))c)))))e))(λde.e)(λde.(d(λfg.g)e))c)) Implementuje algorytm sortowania dla list zakodowanych w kościele. Oznacza to, że wynik: sort (λ c n . (c 3 (c 1 (c 2 n)))) β→ (λ c n . (c 1 (c 2 (c 3 n)))) Podobnie, sort_below …
1
Teoria typów homotopii i twierdzenia o niekompletności Gödla
Twierdzenia Kurta Gödela o niekompletności ustanawiają „nieodłączne ograniczenia wszystkich oprócz najbardziej trywialnych systemów aksomatycznych zdolnych do wykonywania arytmetyki”. Teoria typów homotopii stanowi alternatywną podstawę dla matematyki, podstawę jednoznaczną opartą na wyższych typach indukcyjnych i aksjomat jedności . Książka HoTT wyjaśnia, że typy są wyższe groupoids funkcje są funktory, rodziny typu …
1
Jakie są możliwe implementacje klas typów Haskell i jakie są ich (nie) zalety?
O ile mi wiadomo, funkcja Haskella z ograniczeniami klas typów jest wewnętrznie kompilowana do funkcji z dodatkowymi argumentami, które otrzymują słowniki z niezbędnymi implementacjami poszczególnych klas typów. Czy istnieją inne możliwości kompilowania klas typów? Jeśli tak, jakie są ich (nie) zalety? A jakie kompilatory ich używają?
Korzystając z naszej strony potwierdzasz, że przeczytałeś(-aś) i rozumiesz nasze zasady używania plików cookie i zasady ochrony prywatności.
Licensed under cc by-sa 3.0 with attribution required.