git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2738 from jfdm/naming-adjustments

Renaming Dependent Pairs

commit6dd63938c6786e72044797060c4782584b7b4c6d authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com> dateMon 8 Feb 2016, 16:46 (11 years ago) parent906d921714f514
16 files changed+79−71
compare with master
unifiedsplit
CHANGELOG+4 libs/effects/Effect/Logging/Category.idr+1−1 libs/effects/Effect/Logging/Default.idr+1−1 libs/prelude/Builtins.idr+17−9 libs/prelude/Prelude/Pairs.idr+14−6 libs/prelude/Prelude/Show.idr+1−1 src/Idris/AbsSyntaxTree.hs+4−4 test/disambig002/disambig002.idr+10−12 test/meta002/Tacs.idr+4−5 test/meta002/expected+1−1 test/proof002/Reflect.idr+2−4 test/proof002/expected+1−1 test/proof002/test030.idr−1 test/reg001/reg001.idr+13−14 test/reg064/reg064.idr+6−7 test/unique001/unique001c.idr−4
CHANGELOG+4
@@ -45,6 +45,10 @@ Minor language changes
4545
4646 using (xs : Vect n a)
4747 bad : Elem x xs -> Elem x (y :: xs)
48+* `Sigma` has been renamed to `DPair`.
49+* Accessor functions for dependent pairs have been renamed to bring them into
50+ line with standard accessor functions for pairs. The function `getWitness`
51+ is now `fst`, and `getProof` is `snd`.
4852
4953New in 0.10:
5054============
libs/effects/Effect/Logging/Category.idr+1−1
@@ -147,7 +147,7 @@ logN : (Show a, Eq a) => (l : Nat)
147147 -> (cs : List a)
148148 -> (m : String)
149149 -> Eff () [LOG a]
150−logN l cs msg = call $ Log (getProof lvl) cs msg
150+logN l cs msg = call $ Log (snd lvl) cs msg
151151 where
152152 lvl : (n ** LogLevel n)
153153 lvl = case cast {to=String} (cast {to=Int} l) of
libs/effects/Effect/Logging/Default.idr+1−1
@@ -84,7 +84,7 @@ log l msg = call $ Log l msg
8484||| @l The level to log.
8585||| @m The message to log.
8686logN : (l : Nat) -> {auto prf : LTE l 70} -> (m : String) -> Eff () [LOG]
87−logN l msg = call $ Log (getProof lvl) msg
87+logN l msg = call $ Log (snd lvl) msg
8888 where
8989 lvl : (n ** LogLevel n)
9090 lvl = case cast {to=String} (cast {to=Int} l) of
libs/prelude/Builtins.idr+17−9
@@ -37,17 +37,25 @@ namespace Builtins
3737 %used MkUPair a
3838 %used MkUPair b
3939
40− ||| Dependent pairs
40+ ||| Dependent pairs aid in the construction of dependent types by
41+ ||| providing evidence that some value resides in the type.
4142 |||
42− ||| Dependent pairs represent existential quantification - they consist of a
43− ||| witness for the existential claim and a proof that the property holds for
44− ||| it. Another way to see dependent pairs is as just data - for instance, the
45− ||| length of a vector paired with that vector.
43+ ||| Formally, speaking, dependent pairs represent existential
44+ ||| quantification - they consist of a witness for the existential
45+ ||| claim and a proof that the property holds for it.
4646 |||
47− ||| @ a the type of the witness
48− ||| @ P the type of the proof
49− data Sigma : (a : Type) -> (P : a -> Type) -> Type where
50− MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P
47+ ||| @a the value to place in the type.
48+ ||| @P the dependent type that requires the value.
49+ data DPair : (a : Type) -> (P : a -> Type) -> Type where
50+ MkDPair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> DPair a P
51+
52+ Sigma : (a : Type) -> (P : a -> Type) -> Type
53+ Sigma wit prf = DPair wit prf
54+ %deprecate Sigma "This name is being deprecated in favour of `DPair`."
55+
56+ MkSigma : .{P : a -> Type} -> (x : a) -> (prf : P x) -> DPair a P
57+ MkSigma wit prf = MkDPair wit prf
58+ %deprecate MkSigma "This constructor is being deprecated in favour of `MkDPair`."
5159
5260||| The empty type, also known as the trivially false proposition.
5361|||
libs/prelude/Prelude/Pairs.idr+14−6
@@ -14,7 +14,7 @@ using (a : Type, P : a -> Type)
1414 data Exists : (P : a -> Type) -> Type where
1515 Evidence : .(x : a) -> (pf : P x) -> Exists P
1616
17− ||| Dependent pair where the second field is erased.
17+ ||| Dependent pair where the second field is erased.
1818 data Subset : (a : Type) -> (P : a -> Type) -> Type where
1919 Element : (x : a) -> .(pf : P x) -> Subset a P
2020
@@ -34,12 +34,20 @@ using (a : Type, P : a -> Type)
3434 getProof : (x : Subset a P) -> P (getWitness x)
3535 getProof (Element x pf) = pf
3636
37− namespace Sigma
38− getWitness : Sigma a P -> a
39− getWitness (x ** pf) = x
37+ namespace DPair
38+ fst : DPair a P -> a
39+ fst (x ** pf) = x
4040
41− getProof : (x : Sigma a P) -> P (getWitness x)
42− getProof (x ** pf) = pf
41+ snd : (x : DPair a P) -> P (fst x)
42+ snd (x ** pf) = pf
43+
44+ getWitness : DPair a P -> a
45+ getWitness = fst
46+ %deprecate DPair.getWitness "This is being deprecated in favour of `fst`."
47+
48+ getProof : (x : DPair a P) -> P (fst x)
49+ getProof = snd
50+ %deprecate DPair.getProof "This is being deprecated in favour of `snd`."
4351
4452 -- Polymorphic (class-based) projections have been removed
4553 -- because type-directed name disambiguation works better.
libs/prelude/Prelude/Show.idr+1−1
@@ -192,5 +192,5 @@ Show a => Show (Maybe a) where
192192 showPrec d (Left x) = showCon d "Left" $ showArg x
193193 showPrec d (Right x) = showCon d "Right" $ showArg x
194194
195−(Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where
195+(Show a, {y : a} -> Show (p y)) => Show (DPair a p) where
196196 show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"
src/Idris/AbsSyntaxTree.hs+4−4
@@ -1567,8 +1567,8 @@ falseTy = sUN "Void"
15671567pairTy = sNS (sUN "Pair") ["Builtins"]
15681568pairCon = sNS (sUN "MkPair") ["Builtins"]
15691569
1570−upairTy = sNS (sUN "UPair") ["Builtins"]
1571−upairCon = sNS (sUN "MkUPair") ["Builtins"]
1570+upairTy = sNS (sUN "UPair") ["Builtins"]
1571+upairCon = sNS (sUN "MkUPair") ["Builtins"]
15721572
15731573eqTy = sUN "="
15741574eqCon = sUN "Refl"
@@ -1615,8 +1615,8 @@ modDocName :: Name
16151615modDocName = sMN 0 "ModuleDocs"
16161616
16171617-- Defined in builtins.idr
1618−sigmaTy = sNS (sUN "Sigma") ["Builtins"]
1619−sigmaCon = sNS (sUN "MkSigma") ["Builtins"]
1618+sigmaTy = sNS (sUN "DPair") ["Builtins"]
1619+sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
16201620
16211621piBind :: [(Name, PTerm)] -> PTerm -> PTerm
16221622piBind = piBindp expl
test/disambig002/disambig002.idr+10−12
@@ -6,7 +6,7 @@ Dec0 : Type -> Type
66Dec0 = Dec
77
88Dec1 : {A : Type} -> (P : A -> Type) -> Type
9−Dec1 {A} P = (a : A) -> Dec0 (P a)
9+Dec1 {A} P = (a : A) -> Dec0 (P a)
1010
1111Unique : Type -> Type
1212Unique t = (p : t) -> (q : t) -> p = q
@@ -53,8 +53,8 @@ namespace Finite
5353filterTag : {A : Type} ->
5454 {P : A -> Type} ->
5555 Dec1 P ->
56− Vect n A ->
57− Sigma Nat (\ m => Vect m (Sigma A P))
56+ Vect n A ->
57+ DPair Nat (\ m => Vect m (DPair A P))
5858filterTag d1P Nil = (_ ** Nil)
5959filterTag d1P (a :: as) with (filterTag d1P as)
6060 | (_ ** tail) with (d1P a)
@@ -66,7 +66,7 @@ toVect : {A : Type} ->
6666 {P : A -> Type} ->
6767 Finite A ->
6868 Dec1 P ->
69− (n : Nat ** Vect n (Sigma A P))
69+ (n : Nat ** Vect n (DPair A P))
7070toVect fA d1P = filterTag d1P (toVect fA)
7171
7272sigmaUniqueLemma1 : {A : Type} ->
@@ -74,16 +74,14 @@ sigmaUniqueLemma1 : {A : Type} ->
7474 Unique1 {t0 = A} P ->
7575 (a : A) ->
7676 (p : P a) ->
77− (ss : Vect n (Sigma A P)) ->
78− Elem a (map getWitness ss) ->
77+ (ss : Vect n (DPair A P)) ->
78+ Elem a (map fst ss) ->
7979 Elem (a ** p) ss
8080
8181toVectComplete : {A : Type} ->
8282 {P : A -> Type} ->
83− (fA : Finite A) ->
84− (d1P : Dec1 P) ->
83+ (fA : Finite A) ->
84+ (d1P : Dec1 P) ->
8585 Unique1 {t0 = A} P ->
86− (s : Sigma A P) ->
87− Elem s (getProof (toVect fA d1P))
88−
89−
86+ (s : DPair A P) ->
87+ Elem s (snd (toVect fA d1P))
test/meta002/Tacs.idr+4−5
@@ -208,7 +208,7 @@ namespace STLC
208208
209209 -- Now we put this hole variable into our sigma constructor
210210 -- prior to elaboration, so it doesn't disappear too soon
211− fill `(MkSigma ~(Var tH) ~(Var tmH) : Sigma Ty (Tm []))
211+ fill `(MkDPair ~(Var tH) ~(Var tmH) : DPair Ty (Tm []))
212212 solve
213213 focus tmH
214214 mkTerm [] tm
@@ -287,18 +287,17 @@ namespace STLC
287287 apply `(UnitCon {env=~(Var envH)})
288288 []
289289 solve
290− testElab : Sigma Ty (Tm [])
290+ testElab : DPair Ty (Tm [])
291291 testElab = %runElab (elaborateSTLC (App (Lam "x" UnitCon) UnitCon))
292292
293− testElab2 : Sigma Ty (Tm [])
293+ testElab2 : DPair Ty (Tm [])
294294 testElab2 = %runElab (elaborateSTLC (App (Lam "x" (Var 0)) UnitCon))
295295
296296 -- Doesn't work! :-)
297− testElab3 : Sigma Ty (Tm [])
297+ testElab3 : DPair Ty (Tm [])
298298 testElab3 = %runElab (elaborateSTLC (App (Lam "x" (App (Var 0) (Var 0)))
299299 (Lam "x" (App (Var 0) (Var 0)))))
300300 -- Error is:
301301 -- Tacs.idr line 247 col 14:
302302 -- When elaborating right hand side of testElab3:
303303 -- Unifying ty and Tacs.STLC.ARR ty t would lead to infinite value
304−
test/meta002/expected+1−1
@@ -1,6 +1,6 @@
11Tacs.idr:298:15:
22When checking right hand side of testElab3 with expected type
3− Sigma Ty (Tm [])
3+ DPair Ty (Tm [])
44
55Unifying ty and ARR ty t would lead to infinite value
66AgdaStyleReflection.idr:328:5:
test/proof002/Reflect.idr+2−4
@@ -44,7 +44,7 @@ using (xs : List a, ys : List a, G : List (List a))
4444 let (yl ** (yr, yprf)) = expr_r ey in
4545 appRExpr _ _ xr yr xprf yprf
4646 where
47− appRExpr : (xs', ys' : List a) ->
47+ appRExpr : (xs', ys' : List a) ->
4848 {G : List (List a)} -> {xs, ys : List a} ->
4949 RExpr G xs -> RExpr G ys -> (xs' = xs) -> (ys' = ys) ->
5050 (ws' ** (RExpr G ws', xs' ++ ys' = ws'))
@@ -206,6 +206,4 @@ Reflect.bp1 = proof {
206206-- prover.
207207
208208syntax AssocProof [ty] = quoteGoal x by reflectEq ty [] in
209− getJust (prove (getProof x)) ItIsJust
210−
211−
209+ getJust (prove (snd x)) ItIsJust
test/proof002/expected+1−1
@@ -12,7 +12,7 @@ When checking an application of function Reflect.getJust:
1212 Type mismatch between
1313 IsJust (Just x1) (Type of ItIsJust)
1414 and
15− IsJust (prove (getProof x)) (Expected type)
15+ IsJust (prove (snd x)) (Expected type)
1616
1717 Specifically:
1818 Type mismatch between
test/proof002/test030.idr−1
@@ -10,4 +10,3 @@ total
1010testReflect1 : (xs, ys : List a) ->
1111 ((xs ++ (x :: ys ++ xs)) = ((xs ++ [x]) ++ (ys ++ xs)))
1212testReflect1 {a} xs ys = AssocProof a
13−
test/reg001/reg001.idr+13−14
@@ -37,7 +37,7 @@ filterTagP {n = S m} p (a :: as) q with (p a)
3737 **
3838 ((a ** believe_me Oh)
3939 ::
40− (fst (getProof (filterTagP p as (believe_me Oh)))),
40+ (fst (snd (filterTagP p as (believe_me Oh)))),
4141 Oh
4242 )
4343 )
@@ -95,7 +95,7 @@ mytranspose (x :: y :: xs)
9595
9696using (A : Type, B : A->Type, C : Type)
9797 foo2 : ((x:A) -> B x -> C) -> ((x:A ** B x) -> C)
98− foo2 f p = f (getWitness p) (getProof p)
98+ foo2 f p = f (fst p) (snd p)
9999
100100
101101m_add : Maybe (Either Bool Int) -> Maybe (Either Bool Int) ->
@@ -144,7 +144,7 @@ X : Nat -> Type
144144X t = (c : Nat ** So (c < 5))
145145
146146column : X t -> Nat
147−column = getWitness
147+column = fst
148148
149149data Action = Left | Ahead | Right
150150
@@ -161,31 +161,31 @@ isSubsetOf : Set univ => univ -> univ -> Type
161161isSubsetOf {univ} a b = (c : univ) -> (member c a) -> (member c b)
162162
163163interface Set univ => HasPower univ where
164− Powerset : (a : univ) ->
165− Sigma univ (\Pa => (c : univ) ->
164+ Powerset : (a : univ) ->
165+ DPair univ (\Pa => (c : univ) ->
166166 (isSubsetOf c a) -> member c Pa)
167167
168168powerset : HasPower univ => univ -> univ
169−powerset {univ} a = getWitness (Powerset a)
169+powerset {univ} a = fst (Powerset a)
170170
171171mapFilter : (alpha -> beta) ->
172− (alpha -> Bool) ->
173− Vect n alpha ->
172+ (alpha -> Bool) ->
173+ Vect n alpha ->
174174 (n : Nat ** Vect n beta)
175175mapFilter f p Nil = (_ ** Nil)
176176mapFilter f p (a :: as) with (p a)
177− | True = (_ ** (f a) :: (getProof (mapFilter f p as)))
177+ | True = (_ ** (f a) :: (snd (mapFilter f p as)))
178178 | False = mapFilter f p as
179179
180180hVectEx1 : HVect [String, List Nat, Nat, (Nat, Nat)]
181181hVectEx1 = ["Hello",[1,2,3],42,(0,10)]
182−
182+
183183vecfoo : HVect [String, List Nat, Nat, (Nat, Nat)]
184184vecfoo = put (S (S Z)) hVectEx1
185185
186186foom : Monad m => Int -> m Int
187−foom = pure
188−
187+foom = pure
188+
189189bar : IO ()
190190bar = case foom 5 of
191191 Nothing => print 42
@@ -193,7 +193,7 @@ bar = case foom 5 of
193193
194194Max : (Nat -> Type) -> Type
195195Max p = (Nat , (k : Nat) -> p k -> Nat)
196−
196+
197197maxEquiv : Max p -> (n1 : Nat) -> p n1 -> Nat
198198maxEquiv a n1 pr1 = snd a n1 pr1
199199
@@ -207,4 +207,3 @@ data Kappa : (r : Rho) -> Type where K : Kappa r
207207kappa : Kappa (rho r) -> Kappa (rho r)
208208kappa {r} k = k' where -- k' : Kappa (rho r)
209209 k' = k
210−
test/reg064/reg064.idr+6−7
@@ -1,9 +1,8 @@
1−sigmaEq2 : {A : Type} ->
2− {P : A -> Type} ->
3− {s1: Sigma A P} ->
4− {s2: Sigma A P} ->
5− getWitness s1 = getWitness s2 ->
6− getProof s1 = getProof s2 ->
1+sigmaEq2 : {A : Type} ->
2+ {P : A -> Type} ->
3+ {s1: DPair A P} ->
4+ {s2: DPair A P} ->
5+ fst s1 = fst s2 ->
6+ snd s1 = snd s2 ->
77 s1 = s2
88sigmaEq2 {A} {P} {s1 = (x ** prf)} {s2 = (x ** prf)} Refl Refl = Refl
9−
test/unique001/unique001c.idr−4
@@ -44,7 +44,3 @@ data MPair : AnyType -> AnyType -> AnyType where
4444
4545ndup : {a : UniqueType} -> a -> UPair a a
4646ndup {a} x = (\f : Int -> a => MkUPair (f 0) (f 1)) (uconst x)
47−
48−
49−
50−