User loginNavigation |
archivesA-Posteriori Subtyping: Which Languages?Does anyone know which OO languages support a-posteriori subtyping? In other words the creation of new subtype relationships between classes without modifying existing classes. Thanks a lot! Lambda the Ultimate MacroIn a series of papers, Jean Goubault-Larrecq has established a relationship between modal logic systems and type systems for metaexpressions, i.e. (quasi-)quoted expressions. I will use a pseudo Lisp syntax and furthermore I will write It appears to me that modal operators are merely syntactic abbreviations for predicates on propositions, i.e., (By the way, if we treat predicates/sets as characteristic functions, then modal operators are really evaluators, and |- with two relands is an evaluator with an environment. A partially applied type-assignment relation The proof rules rules for minimal logic in their most basic form (with a single proposition instead of a context) look like the following: (has-type (quote make-x) (quote (|- (quote P)))) (has-type (quote make-y) (quote (|- (quote Q)))) ; ... other assumptions (has-type (quote i→) (quote (∀ a (|- (quote bool)) (∀ b (|- (quote bool)) (→ (→ (|- a) (|- b)) (|- (quote (→ (unquote a) (unquote b))))))))) (has-type (quote e→) (quote (∀ a (|- (quote bool)) (∀ b (|- (quote bool)) (→ (|- (quote (→ (unquote a) (unquote b)))) (→ (|- a) (|- b))))))) Now it becomes clear that proof rules are the types of the constructors of the proofs (terms) in a language. For example, The written representation of an abstraction term is now problematic because the abstraction term contructor We can resort to a trick to be able to write some abstraction terms indirectly. Here the substitution function comes to the rescue. Most generally, Partially applying This explains the strange shape of λ terms: a λ term is actually a macro (i.e. syntactic abbreviation) for a term that cannot be written, somewhat as follows (the output type (defmacro λ (x a m)) (i→ (subst a b x m))) Note the absense of (∀ ... (→λ (quote (λ (unquote x) (unquote a) (unquote m))) (i→ (subst a b x m)))) This explains the shape of the beta reduction rule: (∀ ... (→β (e→ (quote (λ (unquote a) (unquote x) (unquote m))) n) (subst a b x m n))) This is because this rule is merely a special case of a more general rule for beta reduction: (∀ ... (→β (e→ (i→ f) n) (f n))) or, even more generally, (∀ ... (→β (e→ (i→ f)) f)) or even something like: (∀ ... (→β (° e→ i→) id)) By the way, the type assignment rules then become: (has-type (quote t-make-x) (quote (has-type make-x (quote P)))) (has-type (quote t-make-y) (quote (has-type make-y (quote Q)))) ; ... other variable declarations (has-type (quote ti→) (quote (∀ ... (→ (→ (has-type x a) (has-type (f x) b)) (has-type (i→ f) (quote (→ (unquote a) (unquote b)))))))) (has-type (quote te→) (quote (∀ ... (→ (has-type f (quote (→ (unquote a) (unquote b)))) (→ (has-type x a) (has-type (e→ f x) b)))))) By xyzzy at 2006-01-30 17:37 | LtU Forum | login or register to post comments | other blogs | 5638 reads
line breaks?I think it used to be that if I That seems to have gone away, and now |
Browse archivesActive forum topics |
Recent comments
21 weeks 6 days ago
21 weeks 6 days ago
21 weeks 6 days ago
44 weeks 17 hours ago
48 weeks 2 days ago
49 weeks 6 days ago
49 weeks 6 days ago
1 year 3 days ago
1 year 5 weeks ago
1 year 5 weeks ago