tag:blogger.com,1999:blog-8072464059979174136.post4275775444584895571..comments2023-03-31T08:53:17.476-07:00Comments on don't count on finding me: Singleton Types are the Key to Co-dependencyheisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.comBlogger6125tag:blogger.com,1999:blog-8072464059979174136.post-21580217548008411992010-12-21T04:45:26.051-08:002010-12-21T04:45:26.051-08:00In Dylan (an object-oriented functional language)…...<em>In Dylan (an object-oriented functional language)… Here the singleton function returns a type whose sole inhabitant is the argument to singleton.<br /><br />…where values can be lifted up in the type realm and appear at the right-hand-side of the type judgement (:). I prefer to call this co-dependency because it is opposite to regular dependency which happens in the returned expression.</em><br /><br />After pondering on articles and source codes you referenced I must admit I am defeated. I just can not understand how can you mix all of this. :) Dylan (the programming language) has dynamic typing. You seem to use intuitionistic type theory (ITT) (or calculus of inductive constructions, Barendregt's lambda cube, Coq, Agda etc.). IMHO intuitionistic type theory is related to Dylan in no way. No OOP style subtyping. No "type which only inhabitant is a particular number". However, ITT has numbers at the right side of ":". There you also can construct an analogue of your singleton, i.e. an unary predicate which is true only on a single number.<br /><br />The paper by Steven Awodey particularly bewildered me, as it is about ITT in <strong>homotopy theory</strong>. O_Oberoalhttps://www.blogger.com/profile/13229768366613602827noreply@blogger.comtag:blogger.com,1999:blog-8072464059979174136.post-29242955760305457532010-12-14T20:03:01.374-08:002010-12-14T20:03:01.374-08:00These kinds of issues come up frequently in work o...These kinds of issues come up frequently in work on the ML module system, where dependent pairs are used to represent modules and singletons are used to represent type definitions. For example:<br /><br />Extensional Equivalence and Singleton Types.<br />Chris Stone and Robert Harper.<br />http://www.cs.cmu.edu/~rwh/papers/singletons/tocl.pdfDan Licatahttps://www.blogger.com/profile/05419342217317164459noreply@blogger.comtag:blogger.com,1999:blog-8072464059979174136.post-23848899880181894132010-12-14T11:09:10.689-08:002010-12-14T11:09:10.689-08:00"co-dependency" is a bad name. There are..."co-dependency" is a bad name. There are two different things going on in dependent types: first is the ability to lift values into the type level, second is the ability to introduce dependencies between function arguments and their return values (or between the first half of a tuple and the second half). You can have the former without the latter, and many languages which don't support full dependent types do this. That's all you have there in the existential. The quantificand doesn't <i>depend</i> on anything, it just has a value in its type is all.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-8072464059979174136.post-87918834376803088372010-12-14T07:56:06.604-08:002010-12-14T07:56:06.604-08:00@self: s/qualifier/quantifier/g
:-( sorry for the ...@self: s/qualifier/<b>quantifier</b>/g<br />:-( sorry for the confusion...heisenbughttps://www.blogger.com/profile/11328338875953258337noreply@blogger.comtag:blogger.com,1999:blog-8072464059979174136.post-9263321204708338992010-12-14T06:16:08.103-08:002010-12-14T06:16:08.103-08:00@beroal: De Bruijn uses the term "lambda-type...@beroal: De Bruijn uses the term "lambda-typed lambda calculus" (in the title). I did two deliberate changes to this term:<br />1) 'lambda-typed' -> 'qualifier-typed', because in mid-term I intend to support the sigma family, i.e. dependent sums, too (not sure de Bruijn considered these). 'Lambda', at least to me, has the dependent product association.<br />2) I added 'typed' because additionally to the strata and 'degree' (as de Bruijn calls them) I wish to precisely encode the types of terms (such as 42::Int), etc. I do not see yet how this falls out of the paper (I guess he is employing the church encoding of data types).heisenbughttps://www.blogger.com/profile/11328338875953258337noreply@blogger.comtag:blogger.com,1999:blog-8072464059979174136.post-44469460710206111272010-12-14T05:20:36.424-08:002010-12-14T05:20:36.424-08:00Since the last time I wrote about existentials I h...<em>Since the last time I wrote about existentials I had a plenty of time to ponder how they fit into the qualifier-typed typed lambda calculus which de Bruijn has proposed, and I am very proud of implementing a formalization for.</em><br />Can you please point to a specific page in that article that has the phrase "qualifier-typed typed lambda calculus"?beroalhttps://www.blogger.com/profile/13229768366613602827noreply@blogger.com