User loginNavigation |
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 | other blogs | 12186 reads
|
Browse archives
Active forum topics |
Recent comments
12 weeks 1 day ago
12 weeks 1 day ago
12 weeks 1 day ago
34 weeks 2 days ago
38 weeks 4 days ago
40 weeks 2 days ago
40 weeks 2 days ago
42 weeks 6 days ago
47 weeks 4 days ago
47 weeks 4 days ago