User loginNavigation |
GADTs in a dynamically type-checked language?I've been reading papers about Ωmega, and I'm very fascinated by them. At the same time, I'm invested in untyped, dynamically type-checked programming. I'm not sure I want to give it up - it has some conveniences in interactive programming that I consider essential. But is there actually a reason why GADTs wouldn't work in a dynamically type-checked language? FGJω and an extension of C# show that you can encode (some?) uses of GADTs once you have type operators/higher kinds or equational type constraints, respectively. Couple that with exact runtime types as in the CLR and it seems to me that theoretically you could enforce GADT properties even in a dynamically type-checked language. Now, you might ask, what's the point? Let's take the type-safe AST evaluator (yeah, I know... ;)). Well, of course, you'd lose the ability to prevent the construction of ill-formed AST objects at compile-time, but you'd still have these guarantees at run-time. And that would be an improvement over plain dynamically type-checked languages, no? By Manuel J. Simoni at 2010-09-14 02:38 | LtU Forum | previous forum topic | next forum topic | other blogs | 5936 reads
|
Browse archives
Active forum topics |
Recent comments
25 weeks 4 days ago
25 weeks 4 days ago
25 weeks 4 days ago
47 weeks 5 days ago
52 weeks 14 hours ago
1 year 1 week ago
1 year 1 week ago
1 year 4 weeks ago
1 year 8 weeks ago
1 year 8 weeks ago