030317: Marcin: HomoDatoid now defines generic datoids PJ: cleaning up. Files used: HomoDatoid.alfa: Homogenous.alfa, DatoidBase.alfa 030317: Idea - now when generic datoids are coming along, we could replace the Datoid D in DAlgebraic and friends by a code for a set. (That code is enough to obtain the components of a Datoid.) 030316: Marcin: HomoRef now contains reflexivity. PJ: cleaning up. 030314: PJ: Trying to get some Reflexivity to work: Checking Marcins HomoRef.alfa: återvändsgränd liftAnd, liftE, Arity, Sig, Fa, Fa1, F, F1, T, It, DIt, MIt, eq_step_ar, ref_eq_step_ar eq_step', ref_eq_step', eq_step, ref_eq_step eq, - definitionen av ref saknas (återvändsgränd) Homogenous.alfa: Flyttar runt så att HomoRef.alfa inte innhåller dubbletter av Homogenous code. 030311: PJ: More on Recursor-based reflexivity and substitutivity Step 1: Define FIH for ManySorted [non-trivial!] Tools.alfa now contains famOPlus and famOTimes with these helpers FIHx is easy Step 2: Define Fmap for ManySorted Difficult to get the helpers right. But worked. Step 3: Define R for ManySorted Main work was Fmap and getting the type right. Step 4: Express reflexivity using R - stuck on Agda bugs/problems 030304: PJ: Defined (iterator-) equality for ManySorted 030303: PJ: Datoids can be defined for DAlgebraic codes see DAlgebraic/Datoid.alfa But the definition is general recursive - motivation is needed for why it "works". 030208: PJ: eqref NonRec case is harder than expected. Got stuck, talked to Makoto: there is a Better Way! Michael Hedberg has already defined (most) components needed to build complete Datoids (including equality, reflexivity, substitutivity etc.) Thus we could (probably) generalize directly to defining datoid :: (fi::Sig) -> Datoid = ... (T fi) ... datstep :: (fi::Sig) -> Datoid -> Datoid = ... D ... -> ... (F fi D.Elem) ... A requirement is that we absolutely must stick to the (new) alfa library definition of the sigma type (as a signature, not as a data). Relevant pointer (inside the alfa library): SET.alfa (Collapsed) Datoid/DATOID.alfa Datoid/Sum.alfa Collapsed X means that X is essentially a 1-element set A Datoid has a reflexive, substitutive, Boolean equality (substitutivity is very strong - if eq x y then x and y cannot be distinguished by any predicate. Implies symmetry and transitivity.) [Aside: elimEqD may be useful for solving the problem below, but I'll head out for a complete Datoid now instead.] 030208: PJ: Implemented the recursor R for DAlgebraic.alfa Next in line is Reflexive.alfa For annoying reasons (a bug in Agda, I think) the nice definition of eqstepBy using an inner leads to problems in proving the corresponding reflexivity property, so I rewrite eqstepBy (renamed to eqstep) to work around the problem. True (eqstep (nonrec D g) A B r (F1 (nonrec D g) B A f (d,y)) (d,y)) = {- Def. of eqstep and of F1 -} True (eqSigma D (\(d::D.Elem) -> F (g d) A) (\(d::D.Elem) -> F (g d) B) (\(d::D.Elem) -> eqstep (g d) A B r) (d,F1 (g d) B A f y) (d,y)) = {- Def. eqSigma -} True ((\(d::D.Elem) -> eqstep (g d) A B r) d (D.subst ? d d fy) y) where fy = F1 (g d) B A f y = {- Simpl. -} True (eqstep (g d) A B r (D.subst ? d d fy) y) where fy = F1 (g d) B A f y From IH we have what we need module the D.subst eqSigma D (\(d::D.Elem) -> F (g d) A) (\(d::D.Elem) -> F (g d) B) (\(d::D.Elem) -> eqstep (g d) A B r) (d,F1 (g d) B A f y) (d,y)) = {- -} = {- -} We may need a trueSigma? 030204: Patrik Jansson: skissar på bevis av reflexivitet Se Reflexive.alfa 021204: Patrik Jansson (större paket av små ändringar: Klart) Vissa filer använder Lib/SET.alfa och vissa använder MBSet.alfa. Klart förvirrande när meddelanden som "Nat is not equal to Nat" dyker upp. Går detta att ändra enkelt? (vill vi?) (Times i Lib 'r olyckligt definierad - bättre vore en datatyp.) Steg 1: sök efter explicita beroende på MBSet.alfa Algebraic.alfa Algebraic1Par.alfa DAlgebraic.alfa DAlgebraic1Par.alfa DAlgebraic2.alfa DInd.alfa DInd1Par.alfa EqBase.alfa EqZipUtil.alfa IData.alfa IndFam.alfa NitP.alfa Tools.alfa ZipBase.alfa Steg 2: Identifiera i vilken utsträckningen de använder MBSet Byt ut till true, false, zer, suc (Olyckligt att Lib/SET.alfa har Times som ej är data) Inte alls MBSet: Tools, EqBase Båda: ZipBase: oklart vad varifrån *** EqZipUtil: oklart om båda behövs Bara MBSet: NitP, IndFam, IData NitP: Nat, Zero, S, And, Pair@_, Sigma Steg 3: Gör om MBSet till att använda SET.alfa (m.fl.) Fungerar bra. Nu behöver MBSet.alfa inte tas bort (även om den kanske borde byta namn till Prelude.alfa och rensas mer). Steg 4: Testa att alla filer fungerar efter alla dessa småändringar. Klart! 021203: Provar att strukturera upp ManySorted.alfa Det fungerar bra fram till F, F1 och It. 021128: Patrik Jansson Analyzing the generality structure: (and renaming for consistency: Im:=F, SP:=Sig) Homogenous.Sig Iterated.Sig Algebraic.Sig Algebraic1Par.Sig DAlgebraic.Sig DAlgebraic1Par.Sig Infinitary.Sig ManySorted.Sig m *** ej klar IndFam.OP I DInd.OP I DInd1Par.OP I IData.OP I Example dependencies: Even: IndFam ExamplesDAlgebraic2: DAlgebraic2 021128: Zip implemented using It (one-argument iteration) for both DInd1Par and DAlgebraic1Par. The code (in ZipDAlgebraic1Par.alfa) got short and nice after polishing. I decided to swap around arguments so that pure Set arguments ("polymorphism") to functions come first (to enable hiding). This has only been done properly for DAlgebraic1Par but should probably be carried over to the other settings as well. I have not generated any .tex code from the result. I also included equality defined in terms of zip (as proof-of-concept). The natural definition uses Eq A B = A -> B -> Bool ~= A -> B -> Maybe () = Zip A B () Another useful polytypic function (crush) is in CrushDAlgebraic1Par.alfa. 021126: I will start working on Zip using R (or rather It) but before that I cleaned up and sync'ed our file trees. Currently DAlgebraic1Par is missing. What should we do with "Iterated induction"? Where is equality defined using It? In DAlgebraic2.alfa Defined in two steps: 1) A new version of topeq, called topeq' uses the type F (a->Bool) -> F a -> Bool 2) A trivial wrapper topeq2 has type F (T->Bool) -> T -> Bool Not very nice that topeq can't be reused. Let's see if Zip can be done in the same (or a better) way (in DInd1Par) 021126: Overview of files + synchronization of Marcins files and my files. Files I've worked on recently: DInd1Par.alfa ZipBase.alfa ZipDInd1Par.alfa TestZip.alfa MBSet.alfa Tools.alfa NitP.alfa TVec.alfa DInd.alfa Universes I've looked at (and edited): Algebraic1Par.alfa AlgebraicWithoutPar.alfa Other universes: Homogenous1.alfa Homogenous.alfa DAlgebraic2.alfa DAlgebraic.alfa IndFam.alfa IData.alfa Examples: BST.alfa Even.alfa ExamplesDAlgebraic2.alfa Terms.alfa 021106: Factoring the Zip example into separate packages/files The universe construction (code + decode) DInd1Par.alfa Zip for the codes: ZipDInd1Par.alfa A simple test: TestZip.alfa Some prelude/tools: MBSet.alfa Tools.alfa NitP.alfa ZipBase.alfa A vector type (for testing) TVec.alfa 021105: Försöker städa upp i Zip-koden: Identifiera delar -- Nit is intended for a later N-paramater extension Nit, {- Only used as Nit 1 -} nitLift, nitLiftSigma, Pairn {- never used -} -- simpler versions for N=1: pair1 {- never used -}, Sigma1 -- the codes (Im, Im0) use Nit 1 OP, Im, Im0, Im1 Fam, ISet T, out R, R2 sigmaCond Maybe, mapMaybe Zip, zipUnit, trivZip, zipSigma2, zipSigma, zipMaybe, zipPair topzip, zipW, zip -- Example: vectors famV, TVec, VNil, VCons 2, vN2, vB2 zipTVec test1 Compute_me_1 021030: Sammanfattning: Zip definierad för och i DInd1Par.alfa 021030: Försöker definiera om zipSigma till att fungera med en vettigare typ på Zip. Den kommer antagligen att behöva en generaliserad version av sigmaCond men jag börjar för att se var skon klämmer. HL av zipS: if a==a' then Just ? -- här skall det gå att förutsätta a=a' else Nothing OK, zipSigma klar zipPair klar topzip klar(!) Dags för typen på zip och sedan def. typen OK, men R2 måste generaliseras Fixat och även zipW + zip definierat Testar med vektorer av fix längd (där Zip aldrig kan ge Nothing) Verkar fungera som det skall. 021030: OK, topZip är klar + uppstäda (gömda typargument gör att definitionen ser pinsamt enkel ut). Dags att knyta (den rekursiva) knuten och sedan testa resultatet. Modell: DInd: eq och R2 Jag kopierar och modifierar R2 från DInd, men den (R2) måste rensas upp och motiveras någon gång. Den är i varje fall typkorrekt. Problem med zip - det går inte att direkt använda R2 och topzip. Första problemet är att man måste kombinera en mapMaybe Intro med topzip för att få typen rätt på parametern till R2. Det andra problemet är att typen på zip är för begränsad. Redan typen Zip är feltänkt - det skall vara en typ med hål och två fria typparametrar inblandade: Zip1P d a b = d a -> d b -> Maybe (d (a,b)) Detta kräver en jämförelse med Generic Haskell - hur beskriver de typen på zip? [Kollar sid 15 i GH user guide http://www.cs.uu.nl/research/projects/generic-haskell/publications.html] De klarar inte av att definiera en generisk zip annat än för kind *->*. Bra påminnelse är dock att de definierar zipWith direkt - den är mer generell och i någon mening mer naturlig, men den har tre fria typparametrar. ZipW1P d a b c = (a->b->Maybe c) -> d a -> d b -> Maybe (d c) Frågan nu är hur nästa steg skall se ut - skall jag ändra bara till Zip1P eller gå hela vägen till ZipW1P ZipW1P har fler parametrar, men det kanske ändå lönar sig - ofta är det enklare (mindre variation i möjliga alternativ) när det är maximalt parametriserat. I båda fallen blir det en hel del omskrivning av kod. Nåväl, först måste de nya typerna på grundoperationerna skissas: zipUnit :: () -> () -> Maybe () zipPair :: (a1->b1->Maybe c1) -> (a2->b2->Maybe c2) -> ((a1,a2)->(b1,b2)->Maybe (c1,c2)) zipSigma:: (\(a::D)-> B1 a -> B2 a -> Maybe (B3 a)) (Sigma D B1 -> Sigma D B2 -> Maybe (Sigma D B3) zipUnit :: Zip () () () zipPair :: Zip a1 b1 c1 -> Zip a2 b2 c2 -> Zip (And a1 a2) (And b1 b2) (And c1 c2) zipSigma:: (\(a::D)-> Zip (B1 a) (B2 a) (B3 a)) -> (Zip (Sigma D B1) (Sigma D B2) (Sigma D B3) 021030: En viss assymmetri föreligger: Sigma används där PolyP använder Either (binary sum) men fortfarande används "vanlig" produkt, inte Pi där även PolyP använder vanlig produkt. (Fast PolyP är snäppet mer generellt där eftersom Rec och Prod här är kombinerade till bara rec.) Nu när det finns parametrar också är det särskilt tydligt att det finns en inte fullt "faktoriserad" design av kodtypen: både rec och par gör i delvis samma sak (Prod) och delvis sin "egentliga" uppgift (Rec resp. Par). Hur som helst, dags att definiera zipProd och använda den i både rec- och par-fallen. Använder implementationen av Eq från DInd.alfa som modell: därifrån tog jag redan eqSigma och nu är det dags för eqProd. (Jag ser också att eqSigma är lite assymetrisk: den första typparametern levereras tillsammans med sin likhet som en Datoid, medan den andra parametern kommer i två delar (typfamilj + likhetsfamilj). Den senare skulle kunna vara en familj av Datoid, eller så borde även den första plocka isär Datoid till en mängd för sig och en likhetsoperation för sig. (Bättre då att jobba med Datoid.) Det vore snyggt att ha detta som en generell konstruktionsmetod för Datoider (som i Marcins tidigare arbete). Detta bör kunna generaliseras även till andra operationer. (Men då kanske assymetrin i Sigma återkommer - man behöver inte kräva att indexmängden i sigma kan zippas, det räcker med likhet.) 021029: Filar på Patrik/DInd.alfa tills sigmaCond och eq definieras separarat och snyggt (men inte med rekursionskombinator R). Separera ut eqUnit, eqSigma och eqPair i tre egna funktioner som ej hanterar rekursionen över kod-typen OP. Inför typen Eq för läsbarhet. Börjar också arbeta på Zip för DInd1Par.alfa, men behövde den mesta tiden till att rensa upp Eq för att sedan bättre kunna förstå och angripa (den mer kompilcerade) Zip. Implementerar även zipSigma - det återstår den enkla zipProd och den ännu enklare (om allt fungerar) zipPar. Det finns hopp! 021029: Bug i alfa (?): Om man har först har haft (Sigma-)case i ett högerled som visats som patternmatching i vänsterledet, och sedan i ett av fallen tar bort dessa case, så binds ändå dessa argumentspå vänsterledet (nu som variabler, ej Sigma-mönster). 021029: Towards gen. Hinze-style generic prg over dep. types One could probably still see type indexed functions with kind indexed types although at a "higher" level. When writing different versions of the code datatype + decoding functions, a pattern emerges: both Im (and friends) and Eq and Zip all have types with structure inferrable from type of codes. And they all benefit from defining simpler (more "polymorhpic" combinators) to use in the different cases. In Hinze style, binary sum is a constant of "higher kind" - here we have even more esoteric kinds - that of binary sum, for example. I get a feeling this is all related to Ind. red. by Dybjer&Setzer - perhaps I will understand that in the end! There are some argument order/grouping problems with doing it the Hinze style [find a better name]. Joining sets with operations in records may be the best way to go. 021021: zipNonrec :: Zip (Im Xi (nonrec A phi)) = Zip (Sigma A.Elem (\(a::A.Elem) -> Im Xi (phi a))) {- Abstrahera från (Im Xi) till B -} = Zip (Sigma A.Elem (\(a::A.Elem) -> B (phi a))) Intuitivt: (A::Set)(B::A->Set) (a0,a1 :: A)(x::B a0)(y::B a1) (a0,x) (a1,y) | a0==a1 -> mapMaybe (a0,) (någonannanzip x y) | otherwise -> Nothing case (True (a0==a1)) of refl _ -> Im ... (nonrec A f) -> Sigma A.Elem (\(a::A.Elem) -> Im I im (f a)); --------- Datoid = sig ... subst :: Substitutive Elem (\a1 a2->True(a1==a2)) Simplification: subst :: (P::Elem->Set)->(a1,a2::Elem)-> True(a1==a2) -> P a1 -> P a2 can be used to do dependent case: caseOn (c0::C)(c1::B->C)(e::Bool)(f::True e->B) :: C caseOn c0 c1 False f = c0 caseOn c0 c1 True f = c1 (f un) ------ Substitutive (A::Set, R::Rel A) :: Type Substitutive A R = (P::A->Set)->(a1,a2::A)-> R a1 a2 -> P a1 -> P a2 True :: Bool -> Set (interpretation of Bool values as inhabited or empty sets) caseOnPJ (Branch b0) Bool False@_ (\(S::Branch b0) -> rec (phi b0) S b1) (A.eq a0 b0) (\(h::True (A.eq a0 b0)) -> A.subst Branch a0 b0 h a1) caseOnPJ (B::Set)(C::Set)(c0::C)(c1::B -> C)(e::Bool)(f::True e -> B) :: C = case e of { (false) -> c0; (true) -> c1 (f tt@_);} \(h::True (A.eq a0 b0)) -> rec (phi b0) (A.subst Branch a0 b0 h a1) b1) 021017: The equality definition is not using the recursor R - thus its termination needs to be motivated in some other way. (Or it should be redefined in terms of R.) I have changed a few names: using I both for index set and for the main datatype constructor is confusing. Either the index set should be J always or the datatype constructor should change. I decided to implement the second alternative: stick to I for the index set and use T (as for the universal algebra case) for the datatype. I have also tried to order the arguments consistently but this is difficult (see below). 021017: Arbetar om och förstår Marcins kod för generisk programmering över DI DI = inductive families over an arbitrary index set branching on a Datoid (the family compoents may be mutually recursive) DInt.alfa Marcin has defined [J::Set] a datatype of codes for a single datatype in DI: OP J a type of codes for a whole family of d.t. in DI: Fam J = J -> OP J the top level structure type (given interpretations for the indeces, we get an interpretation of OP I (the codes)): Im I im fi a family of datatypes (a translation from a "code family" to a "datatype family"): I J :: Fam J -> (J->Set) a recursion combinator: R There are (at least) two ways of thinking about the first few definitions (order of arguments): Take Im as an example of the first way: (code after) Im_ca :: (I::Set) -> (im::I->Set) -> (fi::OP I) -> Set Reading: Given a set of codes (I) and an interpretation of those codes as sets (im) we give an interpretation of OP I codes as sets. Im_cf :: (I::Set) -> (fi::OP I) -> (im::I->Set) -> Set Reading: given an index set (I) and a code for a datatype (fi) we fill in the recursive wholes with a family of sets to gain a set. Does not flow well. An example of the other way (code first): Im0_cf :: (I::Set) -> (fam::Fam I) -> (im::I -> Set) -> I -> Set Reading: Given an index set (I) and a family of codes (fam), we will lift (improve) a family of sets (im) to a family of sets (by adding a layer of the mutual recursive group of datatypes coded by fam). The fixed point of (Im0 I fam) is a (mutually recursive family of datatypes). Im0_ca :: (I::Set) -> (im::I -> Set) -> (fam::Fam I) -> I -> Set Reading: Given a set of codes (I) and an interpretation of those codes as sets (im) we take a family of codes (fam) to the corresponding family of sets. Natural stratification in the sense that all sets come before the more conctrete data (codes and indeces).