module GMeta2 where {- This module aims at illustrating how GMeta can be extended to support more expressive universes such as the one presented in: Morris, P. and Thorsten Altenkirch and Conor McBride, Exploring the regular tree types, In Types for Proofs and Programs, 2004 The interesting parts of this file are the universe (consisting of the datatypes for representation "Rep" and the interpretations of those representations "Interpret"). This universe is capable of representing mutually inductive definitions. We illustrate this by encoding a simple Tree and Forests example (where the two datatypes are mutually inductively defined) and showing how to embed those datatypes into our universe via an isomorphism. We also show that we can still represent languages with binders by illustrating how to represent the STLC. We then show that with this universe it is possible to define generic operations like substitution. These examples serve the purpose of illustrating that more expressive universes are largely orthogonal to the features for representing binders in GMeta. We do not show a complete library of GMeta here. -} open import Data.Nat -- open import Data.Bool open import Function open import Relation.Nullary open import Relation.Binary open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl) data Ref : ℕ -> Set where VZ : forall {n} -> Ref (suc n) VS : forall {n} -> Ref n -> Ref (suc n) data Rep : ℕ -> Set where REF : forall {n} -> Ref n -> Rep n UNIT : forall {n} -> Rep n PLUS : forall {n} -> Rep n -> Rep n -> Rep n PROD : forall {n} -> Rep n -> Rep n -> Rep n BIND : forall {n} -> Ref n -> Rep n -> Rep n -> Rep n MU : forall {n} -> Rep (suc n) -> Rep n -- shifting representations shiftRef : forall {n} -> Ref n -> Ref (suc n) shiftRef VZ = VZ shiftRef (VS y) = VS (shiftRef y) shiftRep : forall {n} -> Rep n -> Rep (suc n) shiftRep (REF y) = REF (shiftRef y) shiftRep UNIT = UNIT shiftRep (PLUS y y') = PLUS (shiftRep y) (shiftRep y') shiftRep (PROD y y') = PROD (shiftRep y) (shiftRep y') shiftRep (BIND y y' y0) = BIND (shiftRef y) (shiftRep y') (shiftRep y0) shiftRep (MU y) = MU (shiftRep y) vs-inj : forall {n} {r1 r2 : Ref n} -> VS r1 ≡ VS r2 -> r1 ≡ r2 vs-inj refl = refl -- decidability of representations mu-inj : forall {n} {x : Rep (suc n)} {y : Rep (suc n)} -> MU x ≡ MU y -> x ≡ y mu-inj refl = refl eqRef : forall {n} -> Decidable {A = Ref n} _≡_ eqRef VZ VZ = yes refl eqRef VZ (VS _) = no (λ ()) eqRef (VS y) VZ = no (λ ()) eqRef (VS y) (VS y') with eqRef y y' eqRef (VS y) (VS .y) | yes refl = yes refl eqRef (VS y) (VS y') | no prf = no (prf ∘ vs-inj) eqRep : forall {n} -> Decidable {A = Rep n} _≡_ eqRep (REF y) (REF y') with eqRef y y' eqRep (REF y) (REF .y) | yes refl = yes refl eqRep (REF y) (REF y') | no neq = {!!} eqRep (REF y) UNIT = no (λ ()) eqRep (REF y) (PLUS y' y0) = no (λ ()) eqRep (REF y) (PROD y' y0) = no (λ ()) eqRep (REF y) (BIND y' y0 y1) = no (λ ()) eqRep (REF y) (MU y') = no (λ ()) eqRep UNIT (REF y) = no (λ ()) eqRep UNIT UNIT = yes refl eqRep UNIT (PLUS y y') = no (λ ()) eqRep UNIT (PROD y y') = no (λ ()) eqRep UNIT (BIND y y' y0) = no (λ ()) eqRep UNIT (MU y) = no (λ ()) eqRep (PLUS y y') (REF y'') = no (λ ()) eqRep (PLUS y y') UNIT = no (λ ()) eqRep (PLUS y y') (PLUS y0 y1) = {!no (prf ∘ ?) !} eqRep (PLUS y y') (PROD y0 y1) = no (λ ()) eqRep (PLUS y y') (BIND y0 y1 y2) = no (λ ()) eqRep (PLUS y y') (MU y0) = no (λ ()) eqRep (PROD y y') (REF y'') = no (λ ()) eqRep (PROD y y') UNIT = no (λ ()) eqRep (PROD y y') (PLUS y0 y1) = no (λ ()) eqRep (PROD y y') (PROD y0 y1) = {!!} eqRep (PROD y y') (BIND y0 y1 y2) = no (λ ()) eqRep (PROD y y') (MU y0) = no (λ ()) eqRep (BIND y y' y0) (REF y'') = no (λ ()) eqRep (BIND y y' y0) UNIT = no (λ ()) eqRep (BIND y y' y0) (PLUS y1 y2) = no (λ ()) eqRep (BIND y y' y0) (PROD y1 y2) = no (λ ()) eqRep (BIND y y' y0) (BIND y1 y2 y3) = {! !} eqRep (BIND y y' y0) (MU y1) = no (λ ()) eqRep (MU y) (REF y') = no (λ ()) eqRep (MU y) UNIT = no (λ ()) eqRep (MU y) (PLUS y' y0) = no (λ ()) eqRep (MU y) (PROD y' y0) = no (λ ()) eqRep (MU y) (BIND y' y0 y1) = no (λ ()) eqRep (MU y) (MU y') with eqRep y y' eqRep (MU y) (MU .y) | yes refl = yes refl eqRep {n} (MU y) (MU y') | no prf = no (prf ∘ mu-inj) data Tel : ℕ -> Set where tnil : Tel 0 tcons : forall {n} -> Rep n -> Tel n -> Tel (suc n) -- A simple example: a representation for lists RList' : forall {n} -> Rep (suc n) -> Rep n RList' {n} A = MU (PLUS UNIT (PROD A (REF VZ))) -- Interpretation of universes data Interpret : forall {n : ℕ} -> Tel n -> Rep n -> Set where Unit : forall {n} -> {t : Tel n} -> Interpret t UNIT InL : forall {n} {s} {s0} -> {t : Tel n} -> Interpret t s -> Interpret t (PLUS s s0) InR : forall {n} {s} {s0} -> {t : Tel n} -> Interpret t s0 -> Interpret t (PLUS s s0) Pair : forall {n} {s} {s0} -> {t : Tel n} -> Interpret t s -> Interpret t s0 -> Interpret t (PROD s s0) Rec : forall {n} {r} -> {t : Tel n} -> Interpret (tcons (MU r) t) r -> Interpret t (MU r) Top : forall {n} {r} -> { t : Tel n} -> Interpret t r -> Interpret (tcons r t) (REF VZ) Pop : forall {n} {r} {s} -> { t : Tel n} -> Interpret t (REF r) -> Interpret (tcons s t) (REF (VS r)) Var : forall {n} {r} -> {t : Tel n} -> ℕ -> Interpret t (MU r) Bind : forall {n} {s} {s0} -> {t : Tel n} -> ℕ ->(r0 : Ref n) -> Interpret t s -> Interpret t s0 -> Interpret t (BIND r0 s s0) mutual data Tree : Set where C0 : Forest -> Tree data Forest : Set where N1 : Forest C1 : Tree -> Forest -> Forest -- Main Example: representions for Trees and Forests RTree : forall {n} -> Rep n RTree = MU (MU (PLUS UNIT (PROD (REF (VS VZ)) (REF VZ)))) RForest : forall {n} -> Ref (suc n) -> Rep n RForest r = (MU (PLUS UNIT (PROD (REF r) (REF VZ)))) -- RForest = MU (PLUS UNIT (PROD (MU (REF (VS VZ))) (REF VZ))) -- one half of the isomorphism: from functions (mutually defined) mutual FromTree : (n : ℕ) -> (t : Tel n) -> Tree -> Interpret t RTree FromTree n t (C0 y) = Rec (FromForest n t y) FromForest : (n : ℕ) -> (t : Tel n) -> Forest -> Interpret (tcons RTree t) (RForest (VS VZ)) FromForest n t N1 = Rec (InL Unit) FromForest n t (C1 y y') = Rec (InR (Pair (Pop (Top (FromTree n t y))) (Top (FromForest n t y')))) -- the other half of the isomorphism: to functions (mutually defined) mutual ToTree : (n : ℕ) -> (t : Tel n) -> Interpret t RTree -> Tree ToTree n t (Rec y) = C0 (ToForest n t y) ToTree n t (Var y) = C0 N1 ToForest : (n : ℕ) -> (t : Tel n) -> Interpret (tcons RTree t) (RForest (VS VZ)) -> Forest ToForest n t (Rec (InL Unit)) = N1 ToForest n t (Rec (InR (Pair (Pop (Top y)) (Top y')))) = C1 (ToTree n t y) (ToForest n t y') ToForest n t (Var y) = N1 {- data TF : forall {n : ℕ} -> Tel n -> Rep n -> Set -> Set where Ctree : forall {n : ℕ} -> (t : Tel n) -> TF t RTree Tree Cforest : forall {n : ℕ} -> (t : Tel n) -> TF (tcons RTree t) (RForest (VS VZ)) Forest ToTF : (n : ℕ) -> (t : Tel n) -> (r : Rep n) -> (typ : Set) -> TF t r typ -> Interpret t r -> typ ToTF n t .(MU (MU (PLUS UNIT (PROD (REF (VS VZ)) (REF VZ))))) .Tree (Ctree .t) (Rec y) = C0 (ToTF (suc n) (tcons RTree t) (RForest (VS VZ)) Forest (Cforest t) y) ToTF n t .(MU (MU (PLUS UNIT (PROD (REF (VS VZ)) (REF VZ))))) .Tree (Ctree .t) (Var y) = C0 N1 ToTF .(suc n) .(tcons (MU (MU (PLUS UNIT (PROD (REF (VS VZ)) (REF VZ))))) t) .(MU (PLUS UNIT (PROD (REF (VS VZ)) (REF VZ)))) .Forest (Cforest {n} t) (Rec (InL Unit)) = N1 ToTF .(suc n) .(tcons (MU (MU (PLUS UNIT (PROD (REF (VS VZ)) (REF VZ))))) t) .(MU (PLUS UNIT (PROD (REF (VS VZ)) (REF VZ)))) .Forest (Cforest {n} t) (Rec (InR (Pair (Pop (Top y)) (Top y')))) = C1 (ToTF n t RTree Tree (Ctree t) y) (ToTF (suc n) (tcons RTree t) (RForest (VS VZ)) Forest (Cforest t) y') ToTF .(suc n) .(tcons (MU (MU (PLUS UNIT (PROD (REF (VS VZ)) (REF VZ))))) t) .(MU (PLUS UNIT (PROD (REF (VS VZ)) (REF VZ)))) .Forest (Cforest {n} t) (Var y) = N1 -} -- ToTree n t (Rec (Rec (InL Unit))) = C0 N1 -- ToTree n t (Rec (Rec (InR (Pair (Pop (Top y)) (Top y'))))) = C0 (C1 (ToTree n t y) {!!}) -- ToTree n t (Rec (Var y)) = {!!} -- ToTree n t (Var y) = {!!} lookup : forall {n} -> Ref n -> Tel n -> Rep n lookup VZ (tcons y y') = shiftRep y lookup (VS y) (tcons y' y0) = shiftRep (lookup y y0) -- Representing the simply typed lambda-calculus RType : forall {n} -> Rep n RType = MU (PLUS UNIT (PROD (REF VZ) (REF VZ))) RTerm : forall {n} -> Rep n RTerm = MU (PLUS (PROD (REF VZ) (REF VZ)) (BIND VZ RType (REF VZ))) -- RType : Rep (suc n) Type = Interpret tnil RType GType : forall {n} -> {t : Tel n} -> Set GType {n} {t} = Interpret t RType -- STLC data LType : Set where U : LType Arrow : LType -> LType -> LType fromType : forall {n} -> {t : Tel n} -> LType -> Interpret t RType fromType U = Rec (InL Unit) fromType (Arrow y y') = Rec (InR (Pair (Top (fromType y)) (Top (fromType y')))) toType : forall {n} -> {t : Tel n} -> Interpret t RType -> LType toType (Rec (InL Unit)) = U toType (Rec (InR (Pair (Top y) (Top y')))) = Arrow (toType y) (toType y) toType (Var y) = U data LTerm : Set where BVar : ℕ -> LTerm Lam : ℕ -> LType -> LTerm -> LTerm App : LTerm -> LTerm -> LTerm fromTerm : forall {n} -> {t : Tel n} -> LTerm -> Interpret t RTerm fromTerm (BVar y) = Var y fromTerm (Lam x y y') = Rec (InR (Bind x _ (fromType y) (Top (fromTerm y')))) fromTerm (App y y') = Rec (InL (Pair (Top (fromTerm y)) (Top (fromTerm y')))) toTerm : forall {n} -> {t : Tel n} -> Interpret t RTerm -> LTerm toTerm (Rec (InL (Pair (Top y) (Top y')))) = App (toTerm y) (toTerm y') toTerm (Rec (InR (Bind x .VZ y (Top y')))) = Lam x (toType y) (toTerm y') toTerm (Var y) = BVar y myterm = Lam 0 U (BVar 0) unit : Type unit = Rec (InL Unit) arrow : Type -> Type -> Type arrow t1 t2 = Rec (InR (Pair (Top t1) (Top t2))) eqTel : forall {n} -> Decidable {A = Tel n} _≡_ eqTel tnil tnil = yes refl eqTel (tcons y y') (tcons y0 y1) with eqRep y y0 eqTel (tcons y y') (tcons .y y1) | yes refl with eqTel y' y1 eqTel (tcons y y') (tcons .y .y') | yes refl | yes refl = yes refl eqTel (tcons y y') (tcons .y y1) | yes refl | no neq = no {!!} eqTel (tcons y y') (tcons y0 y1) | no neq = no {!!} -- substitution fsubst : forall {n} {r1} {t1 : Tel n} {m} {r2} {t2 : Tel m} -> ℕ -> Interpret t1 r1 -> Interpret t2 r2 -> Interpret t2 r2 fsubst v M Unit = Unit fsubst v M (InL y) = InL (fsubst v M y) fsubst v M (InR y) = InR (fsubst v M y) fsubst v M (Pair y y') = Pair (fsubst v M y) (fsubst v M y') fsubst v M (Rec y) = Rec (fsubst v M y) fsubst v M (Top y) = Top (fsubst v M y) fsubst v M (Pop y) = Pop (fsubst v M y) fsubst {n} {_} {_} {m} {MU r} {_} v M (Var y) with n ≟ m fsubst {n} {r1} {_} {.n} {MU r2} {_} v M (Var y) | yes refl with eqRep r1 (MU r2) fsubst {n} {MU r1} {_} {.n} {MU .r1} {_} v M (Var y) | yes refl | yes refl with v ≟ y fsubst {n} {MU r1} {t1} {.n} {MU .r1} {t2} v M (Var .v) | yes refl | yes refl | yes refl with eqTel t1 t2 fsubst {n} {MU r1} {t1} {.n} {MU .r1} {.t1} v M (Var .v) | yes refl | yes refl | yes refl | yes refl = M fsubst {n} {MU r1} {t1} {.n} {MU .r1} {t2} v M (Var .v) | yes refl | yes refl | yes refl | no neq = Var v fsubst {n} {MU r1} {_} {.n} {MU .r1} {_} v M (Var y) | yes refl | yes refl | no neq = Var y fsubst {n} {_} {_} {.n} {MU r1} {_} v M (Var y) | yes refl | yes x = Var y fsubst {n} {r1} {t2} {.n} {MU r2} {_} v M (Var y) | yes refl | no neq = Var y fsubst {n} {_} {_} {m} {MU r} {_} v M (Var y) | no prf = Var y fsubst {n} {r1} {_} {m} {.(BIND r0 s s0)} {t2} v M (Bind {.m} {s} {s0} x r0 y y') with n ≟ m fsubst {.m} {r1} {_} {m} {.(BIND r0 s s0)} {t2} v M (Bind {.m} {s} {s0} x r0 y y') | yes refl with eqRep (lookup r0 t2) r1 fsubst {.m} {.(lookup r0 t2)} {_} {m} {.(BIND r0 s s0)} {t2} v M (Bind {.m} {s} {s0} x r0 y y') | yes refl | yes refl with v ≟ x fsubst {.m} {.(lookup r0 t2)} {_} {m} {.(BIND r0 s s0)} {t2} .x M (Bind {.m} {s} {s0} x r0 y y') | yes refl | yes refl | yes refl = Bind x r0 (fsubst x M y) y' fsubst {.m} {.(lookup r0 t2)} {_} {m} {.(BIND r0 s s0)} {t2} v M (Bind {.m} {s} {s0} x r0 y y') | yes refl | yes refl | no neq = Bind x r0 (fsubst v M y) (fsubst v M y') fsubst {.m} {r1} {_} {m} {.(BIND r0 s s0)} {t2} v M (Bind {.m} {s} {s0} x r0 y y') | yes refl | no neq = Bind x r0 (fsubst v M y) (fsubst v M y') fsubst {n} {r1} {_} {m} {.(BIND r0 s s0)} {t2} v M (Bind {.m} {s} {s0} x r0 y y') | no neq = Bind x r0 (fsubst v M y) (fsubst v M y')