In Sprachen wie Agda, Idris oder Haskell mit Typ-Erweiterungen gibt es eine = Typen Art wie die folgenden`Refl 'Ding in der Kalkül der Konstruktionen?
data a :~: b where
Refl :: a :~: a
a :~: b bedeutet, dass a und b gleich sind.
Kann ein solcher Typ in calculus of constructions oder Morte definiert werden (was ist die Programmiersprache, die auf der Konstruktionskalkulation basiert)?
Die Standard-Kirche-Codierung von a :~: b in CoC ist:
(a :~: b) =
forall (P :: * -> * -> *).
(forall c :: *. P c c) ->
P a b
Refl
Refl a :: a :~: a
Refl a =
\ (P :: * -> * -> *)
(h :: forall (c::*). P c c) ->
h a
sein Die formuliert über die Gleichstellung von Typen. Für die Gleichheit zwischen Terms, die :~: Beziehung muss ein zusätzliches Argument t :: *, wo a b :: t.
Faszinierend. Ist es möglich, einen Widerspruch von "0: ~: 1" abzuleiten, wie in den anderen Sprachen? (Oh, Moment mal, ich sehe wie. Machen Sie einfach eine Gleichheitsfunktion, die '()' anstelle von True und 'Void' anstelle von false zurückgibt. Ich denke, das würde funktionieren.) – PyRulez
(Ich sehe auch, wie dies leicht auf andere GADTs verallgemeinert wird .) – PyRulez
@PyRulez Ja. Mit Kirchenziffern sind '0 f x = x' und '1 f x = f x' (modulo zusätzliche Argumente). Mit diesem können Sie '0 (const True) False = False 'und' 1 (const True) False = True' haben. Nehmen wir '0: ~: 1' an und nehmen' P x y = (x (const True) False) <-> (y (const True) False) ', können wir' False <-> True 'beweisen. – chi
Jeder induktive Typ kann in CoC codiert werden, aber ohne zugehöriges _abhängiges_ Eliminierungsprinzip (eine nicht abhängige Eliminierung ist möglich). (Beachten Sie auch, dass 'a: ~: b 'ein Typ ist, aber' Refl 'ein Wert ist.) – chi
Das Kalkül von Konstruktionen ist die" Spitze "des Lambda-Würfels. Haskell, Agda und Idris sind "unter" CoC. Daher sollte die einfache Tatsache, dass CoC expressiver ist, möglich sein. (Jemand könnte darauf hinweisen, wenn ich falsch in diesem Abzug bin?) – Bakuriu
@Bakuriu Eigentlich sind Agda/Coq jenseits CoC, da sie auch induktive Typen mit abhängiger Eliminierung erlauben, die CoC fehlt. Agda beweist auch Streichers Axiom K, was besagt, dass zwei beliebige Beweise "p, q" der gleichen Gleichheit "a = b" gleich sein müssen ("p = q") - nicht verfügbar in CoC oder Coq (auch bekannt als CiC). – chi