- From: Ivan Herman <ivan@w3.org>
- Date: Thu, 17 Feb 2011 15:47:31 +0100
- To: Alexandre Bertails <bertails@w3.org>
- Cc: Juan Sequeda <juanfederico@gmail.com>, RDB2RDF WG <public-rdb2rdf-wg@w3.org>, "ericP@w3.org Prud'hommeaux" <ericp@w3.org>
- Message-Id: <33118BD1-9E9C-46F3-95D7-07100B3C6CFB@w3.org>
Alex, On Feb 17, 2011, at 15:28 , Alexandre Bertails wrote: [snip] >> >> A specific technical question and this probably shows my lack of sql knowledge. The DM document talks about primary keys as possibly a multi-column primary keys (eg, section 2.2). Your description says >> >> primaryKey : Table → {s:Set(CandidateKey) | size(s) ≤ 1} > > No, this is actually perfectly correct. I will of course explain that in > an introduction but here is a quick explanation of what this dependent > type [1] means. > > The general form of a dependent type is { a:A | P(a) } where P is a > predicate on a. It's read "the set of a of type A such that P(a)". > > If you want to understand the basic meaning, start by removing the > dependent part and you obtain: > primaryKey : Table → Set(CandidateKey) > > So primaryKey is a function giving you a set of CandidateKey from a > Table, potentially empty. But we *know* we want to restrict this type to > a set with at most 1 element (there is 0 or only 1 primary key). This is > where the dependent type gives you the information. First you bind the > Set to s, then you can use it with a predicate constraining the size, > expecting than the function "size" is part of the accessors associated > with the commonly known Set ADT. > You misunderstood me. I understand the formalism, I guess. But does that specification means that for every table t, primaryKey(t) will give me a set s=primaryKey(t) where size(s)<=1? Ie, that, for every table, the primaryKey is either empty or restricted to one single column? That is the discrepancy with section 2.2 that explicitly speaks about multi-column primary keys... [snip] > >> ------------- >> >> I understand the intention, but I am not sure I fully understand the mathematical formalism in, say, >> >> references : {t:Table} → {r:Row | r ∈ t} → Set(ForeignKey) >> >> The formalism you use for accessor functions like >> >> bla : {a:Set1} → {b:Set2} >> >> seems to indicate that this is a function so that bla(a) yields b. But I am not sure what the value of references(t) is... Shouldn't it be >> >> references : {t:Table} → {r:Row | r ∈ t} → { f:Set(ForeignKey) | (cn,v) ∈ r | (cn,t1,c1) ∈ r} >> >> or something like that? >> >> (The same issue with 'lexicals' and 'scalars'.) > > Each time you '{' '}' in a type, be sure it *is* a dependent type. > > That's known as type-as-specification. We say that the function is fully > specified. Here, it's really mandatory because I need some information > that binds Table and Row, the later needing to be part of the body of > the table. That exactly what the type means. > > Again, first remove all the dependent-types and try to understand what > kind of constraints you need: > > references : Table → Row → Set(ForeignKey) Yes. But isn't it correct that for the result you _do_ need constraints, something that I tried to capture in my row? The way you say does not tell me what kinds of constraints you need to impose on the 'results'... [snip] > > I also applied s/tuple/row/ . The document is updated. > I will look at it... later:-) Cheers Ivan > Thanks again Ivan! > > Alexandre. > > [1] http://en.wikipedia.org/wiki/Dependent_type > > > >> >> ---- >> Ivan Herman, W3C Semantic Web Activity Lead >> Home: http://www.w3.org/People/Ivan/ >> mobile: +31-641044153 >> PGP Key: http://www.ivan-herman.net/pgpkey.html >> FOAF: http://www.ivan-herman.net/foaf.rdf >> >> >> >> >> > > ---- Ivan Herman, W3C Semantic Web Activity Lead Home: http://www.w3.org/People/Ivan/ mobile: +31-641044153 PGP Key: http://www.ivan-herman.net/pgpkey.html FOAF: http://www.ivan-herman.net/foaf.rdf
Attachments
- application/pkcs7-signature attachment: smime.p7s
Received on Thursday, 17 February 2011 14:46:35 UTC