User loginNavigation |
Static Types vs. Partially Evaluated Latent TypesHere's a question I've promoted from another thread (sorry for the multiple postings). What's the difference between static type inference (like in Haskell) and a latent (tagged) type system (think Scheme) with a real good partial evaluator? In the type-inference situation, we're using unification to solve a set of constraints. If there's no solution, we give up and say the program was ill-typed. On the other hand, it seems like tag checking code in a latently typed lanugage would be a good candidate to get partially evaluated away at compile time. For example it seems like... ;; typed values are really pairs of values and types ;; e.g. (123 . 'number) ;; ("abc" . 'string) (define (isnumber n) (eq? (cdr n) 'number)) (define (add arg1 arg2) (if (and (isnumber arg1) (isnumber arg2)) (machine-add (car arg1) (car arg2)) (error "not a number"))) (add '(4 . number) '(5 . number))...should be easily changed into... (machind-add 4 5)... And after we're done partially evaluating our source, if we still have left over type-check predicates like 'isnumber' in the code then we again declare that the program is ill-typed. Are the two methods comparable in any way? Is one method more powerful than the other, or are they somehow duals of each other? Are there any papers available discussing this?
Anton van Straaten recommends looking at a previous typing thread, and the paper Types as Abstract Interpretations, as well as a posting of his to the LL mailing list. Any futher thoughts? By Greg Buchholz at 2005-06-23 20:41 | LtU Forum | previous forum topic | next forum topic | other blogs | 7495 reads
|
Browse archives
Active forum topics |
Recent comments
16 weeks 1 day ago
16 weeks 2 days ago
16 weeks 2 days ago
38 weeks 3 days ago
42 weeks 5 days ago
44 weeks 2 days ago
44 weeks 2 days ago
47 weeks 6 hours ago
51 weeks 4 days ago
51 weeks 4 days ago