Trong các ngôn ngữ như Agda, Idris, hoặc Haskell với phần mở rộng loại hình, có một = loại loại giống như các`Điều` phản ánh trong Calculus of Constructions?
data a :~: b where
Refl :: a :~: a
a :~: b nghĩa là a và b đều giống nhau.
Loại như vậy có thể được xác định trong calculus of constructions hoặc Morte (ngôn ngữ lập trình dựa trên tính toán xây dựng) không?
Tiêu chuẩn Giáo-mã hóa của a :~: b trong CoC là:
(a :~: b) =
forall (P :: * -> * -> *).
(forall c :: *. P c c) ->
P a b
Refl là
Refl a :: a :~: a
Refl a =
\ (P :: * -> * -> *)
(h :: forall (c::*). P c c) ->
h a
Trên đây formulates bình đẳng giữa loại. Đối với sự bình đẳng giữa các điều khoản , quan hệ :~: phải có đối số bổ sung t :: *, trong đó a b :: t.
((:~:) t a b) =
forall (P :: t -> t -> *).
(forall c :: t. P c c) ->
P a b
Refl t a :: (:~:) t a a
Refl t a =
\ (P :: t -> t -> *)
(h :: forall (c :: t). P c c) ->
h a
Hấp dẫn. Có thể lấy được mâu thuẫn từ '0: ~: 1', giống như bạn có thể làm bằng các ngôn ngữ khác không? (Oh chờ đợi, tôi thấy như thế nào. Chỉ cần tạo một hàm bình đẳng trả về '()' thay vì True và 'Void' thay vì false. Tôi nghĩ nó sẽ hoạt động.) – PyRulez
(Ngoài ra, tôi thấy cách này dễ dàng khái quát hóa với các GADT khác .) – PyRulez
@PyRulez Có. Với số nhà thờ, '0 f x = x' và' 1 f x = f x' (modulo đối số kiểu bổ sung). Sử dụng điều đó, bạn có thể có '0 (const True) False = False' và' 1 (const True) False = True'. Giả sử '0: ~: 1' và lấy' P x y = (x (const True) False) <-> (y (const True) False) ', chúng ta có thể chứng minh' False <-> True'. – chi
Mọi loại quy nạp có thể được mã hóa trong CoC, nhưng không có nguyên tắc loại trừ _dependent_ (loại trừ không phụ thuộc). (Cũng lưu ý rằng 'a: ~: b' là một kiểu, nhưng' Refl' là một giá trị.) – chi
Tính toán của các công trình là "đỉnh" của khối lambda. Haskell, Agda và Idris là "dưới đây" CoC. Do đó, nó phải là có thể cho thực tế đơn giản là CoC là biểu cảm hơn. (Ai đó có thể chỉ ra nếu tôi sai trong khoản khấu trừ này?) – Bakuriu
@ Bakuriu Trên thực tế, Agda/Coq vượt quá CoC vì chúng cũng cho phép loại quy nạp với loại bỏ phụ thuộc, mà CoC thiếu. Agda cũng chứng minh tiên đề của Streicher K, ngụ ý rằng hai bằng chứng 'p, q' của cùng một đẳng thức' a = b' phải bằng nhau ('p = q') - không có trong CoC hoặc Coq (hay còn gọi là CiC). – chi