User loginNavigation |
Type TheoryLightweight Static Capabilitites (II)The slides for the talk discussed here are now available for download. Like all of Ken and Oleg's work, this stuff is both cool and important. Keep in mind that the talk is quite different from the paper. The safety claims were formalized and proved in Twelf: list example, array example. To follow the proofs you should read them alongside the presentation slides. I am told that the first file might change soon, to reflect a more general proof. Perhaps Ken or Oleg would like to comment on the experience of doing mechanized proofs, a subject the comes up regularly on LtU. LtU newcomers, who already managed to take in a little Haskell or ML, may want to spend a little time chewing on this, and ask questions if something remains unclear, since this work may eventually have practical importance, and can teach quite a few interesting techniques. By Ehud Lamm at 2006-08-29 08:34 | Semantics | Software Engineering | Type Theory | 1 comment | other blogs | 8889 reads
Ivor, a proof engineI found an interesting new paper by Edwin Brady.
By Niels Hoogeveen at 2006-08-08 13:39 | Functional | Lambda Calculus | Type Theory | 1 comment | other blogs | 6850 reads
Interface AutomataInterface Automata
The idea of expressing order of message exchange as type is certainly not new (as anyone exposed to web service choreography hype can tell - oh, just kidding, of course the theory is much older). However, the specific approach looks interesting (not the least because of appealing to game semantics). By Andris Birkmanis at 2006-07-24 17:32 | Semantics | Type Theory | 4 comments | other blogs | 7151 reads
Lightweight Static CapabilitiesLightweight Static Capabilitites
Pursuant to this thread about the membrane pattern in static languages from Mark Miller's excellent Ph.D. thesis. I don't yet know whether a solution is derivable from this work, but Mark was kind enough to point me to it, and Oleg seems to want to see it distributed, so here it is—Mark and/or Oleg, please let me know if this is premature. By Paul Snively at 2006-07-23 19:50 | Semantics | Type Theory | 17 comments | other blogs | 23920 reads
Concoqtion: Mixing Indexed Types and Hindley-Milner Type InferenceFrom the "Whoa!" files: Concoqtion: Mixing Indexed Types and Hindley-Milner Type Inference
Another tough-to-categorize one: dependent types, the Curry-Howard Correspondence, logic programming, theorem provers as subsystems of compilers, implementation issues... it's all in here. Update: A prototype implementation is available here, but it took a bit of Google-fu to find, and it's brand new, so be gentle. Update II: The prototype implementation isn't buildable out of the box, and includes a complete copy of both the Coq and O'Caml distributions, presumably with patches etc. already applied. So it's clearly extremely early days yet. But this feels very timely to me, perhaps because I've just started using Coq within the past couple of weeks, and got my copy of Coq'Art and am enjoying it immensely. Update III: It occurs to me that this might also relate to Vesa Karvonen's comment about type-indexed functions, which occurs in the thread on statically-typed capabilities, so there might be a connection between this front-page story and the front-page story on lightweight static capabilities. That thought makes me happy; I love it when concepts converge. By Paul Snively at 2006-07-23 18:15 | Functional | Implementation | Logic/Declarative | Semantics | Type Theory | 3 comments | other blogs | 12080 reads
A Core Calculus for Scala Type CheckingA Core Calculus for Scala Type Checking, is a new paper by the Scala team.
The paper revolves around the question of decidability of type checking in Scala. The following quote summarizes the background of this question.
Ehud: Given current interest in Scala and its more or less unique (don't want to raise controversy here) position as being both a functional and an OO language, furthermore being much more than a toy language, would it be a good idea to give Scala a place in the Spotlight section? By Niels Hoogeveen at 2006-07-14 12:01 | Object-Functional | Type Theory | 16 comments | other blogs | 14450 reads
Securing the .NET Programming ModelSecuring the .NET Programming Model. Andrew J. Kennedy.
This is highly amusing stuff, of course. Some choice quotes:
To see the six problems identified by thinking about full abstraction you'll have to go read the paper... By Ehud Lamm at 2006-06-26 11:17 | Implementation | OOP | Semantics | Type Theory | 14 comments | other blogs | 14832 reads
Variance and Generalized Constraints for C# GenericsVariance and Generalized Constraints for C# Generics. Burak Emir, Andrew J. Kennedy, Claudio Russo, Dachuan Yu. July 2006
Discussion of previous C# GADT paper on LtU. I am unsure about use-site versus definition-site variance declerations. It would be interesting to hear what others think. Also check out the LtU discussion on wildcards in Java. By Ehud Lamm at 2006-06-18 11:33 | OOP | Software Engineering | Type Theory | 16 comments | other blogs | 20964 reads
Sage: A Programming Language With Hybrid Type-CheckingSince we've been discussing hybrid type checking, dependent types, etc. recently...
By Paul Snively at 2006-06-04 23:52 | Functional | Implementation | Meta-Programming | Type Theory | 5 comments | other blogs | 14720 reads
Type inference for PythonThe subject of type inference for dynamically-checked languages came up in the Buried Treasure thread. A question was raised in that thread having to do with why static type inference in these languages is difficult. Since there's a nascent body of literature which addresses that question, here are a few links to articles and papers about type inference for Python. A nice overview can be found in Localized Type Inference of Atomic Types in Python, a Master's thesis by Brett Cannon. The whole thesis is relevant, but for an overview of the issues, see Chapter 3, "Challenges of Inferring Types in Python". Chapter 4 summarizes previous attempts involving static inference in Python, including Psyco (previously on LtU) and Starkiller. The limitations of these attempts are briefly addressed. Type inference solutions for Python invariably involve restrictions to make the problem tractable. The above paper focuses on "inferring atomic types in the local namespace". Another approach is described in Aggressive Type Inference, by John Aycock. Aycock makes an important observation:
The article offers a type inference approach which exploits this observation. (If the meaning of the above quote isn't clear, I recommend reviewing our mammoth three-part thread on the subject, "Why type systems are interesting", part I, part II, and part III.) The PyPy implementation of Python in Python (previously on LtU) uses a restricted subset of Python, called RPython, to implement parts of the language. RPython is sufficiently static to be able to support full-program type inference. It is not a "soft" inference approach, and is not designed to be used with ordinary Python programs. The paper Compiling dynamic language implementations covers the approach used for static analysis of RPython. The PyPy Coding Guide, starting at section 1.4 may also be useful. (It may be interesting to note that the PyPy approach is very similar to that used previously for Scheme 48. The core of Scheme 48 is implemented in PreScheme, a subset of Scheme that supports full-program type inference.) Finally, Guido van Rossum has a number of blog entries on the subject of adding optional static typing to Python:
If anyone knows of any other good treatments of type inference in Python or similar languages, please post links here. By Anton van Straaten at 2006-05-30 01:54 | Python | Type Theory | 18 comments | other blogs | 55948 reads
|
Browse archives
Active forum topics
|
Recent comments
14 weeks 5 days ago
19 weeks 17 hours ago
20 weeks 4 days ago
20 weeks 4 days ago
23 weeks 2 days ago
28 weeks 3 hours ago
28 weeks 4 hours ago
28 weeks 3 days ago
28 weeks 3 days ago
31 weeks 1 day ago