W językach takich jak Agda, Idris lub Haskell z rozszerzeniami typu, istnieje = typ coś w rodzaju poniższej`Refl` rzecz w rachunku kosztów budowy?
data a :~: b where
Refl :: a :~: a
a :~: b oznacza, że a i b są takie same.
Czy taki typ można zdefiniować w calculus of constructions lub Morte (który jest językiem programowania opartym na rachunku budowy)?
Church standard kodowania z a :~: b w KU jest:
(a :~: b) =
forall (P :: * -> * -> *).
(forall c :: *. P c c) ->
P a b
Refl jest
Refl a :: a :~: a
Refl a =
\ (P :: * -> * -> *)
(h :: forall (c::*). P c c) ->
h a
Powyższy formułuje równości typów. Aby uzyskać równość między warunkami, relacja :~: musi przyjąć dodatkowy argument t :: *, gdzie a b :: t.
Intrygujące. Czy można uzyskać sprzeczność z '0: ~: 1', tak jak w innych językach? (Och, czekaj, widzę, jak to zrobić, po prostu wykonaj funkcję równości, która zwraca '()' zamiast True i 'Void' zamiast false.Myślę, że to zadziała.) – PyRulez
(Widzę też, jak łatwo to uogólnić na inne GADTs .) – PyRulez
@PyRulez Tak. Z kościelnymi cyframi, '0 f x = x' i' 1 f x = f x' (modulo dodatkowe argumenty typu). Używając tego, możesz mieć '0 (const True) False = False' i' 1 (const True) False = True'. Zakładając '0: ~: 1' i biorąc' P x y = (x (const True) False) <-> (y (const True) False) ', możemy udowodnić' False <-> True'. – chi
Każdy typ indukcyjny może być kodowany w CoC, ale bez powiązanej zasady _dependent_ eliminacji (dostępna jest eliminacja zależna). (Zwróć także uwagę, że 'a: ~: b' jest typem, ale' Refl' jest wartością.) – chi
Rachunek konstrukcji jest "szczytem" kostki lambda. Haskell, Agda i Idris są "poniżej" CoC. Dlatego powinno być możliwe z prostego faktu, że CoC jest bardziej ekspresyjny. (Ktoś mógłby wskazać, czy się mylę w tym odliczeniu?) – Bakuriu
@Bakuriu W rzeczywistości, Agda/Coq są poza CoC, ponieważ umożliwiają one również typy indukcyjne z zależną eliminacją, której brakuje w CoC. Agda dowodzi także aksjomatu Streichera K, co oznacza, że dwa dowolne dowody "p, q" o tej samej równości 'a = b' muszą być równe (' p = q') - niedostępne w CoC lub Coq (aka CiC). – chi