On Fri, Jun 12, 2015 at 3:56 AM, Keean Schupke <[email protected]> wrote: > On 12 Jun 2015 08:19, "Matt Oliveri" <[email protected]> wrote: >> Well if you're just trying to enforce that ASTs are of well-typed >> program fragments, this is not true. There's a certain point after >> which you can encode any language's typing rules in the host type >> system. This is analogous to how you only need predicate logic to >> axiomatize any deductive system. > > I'm not sure I get this. Let's say my language has intersection types, which > require unification with expansion variables, and I am writing the compiler > in Haskell. How / why would I want to encode that into the Haskell type > system which does not.
I said there's a certain point after which you can encode any language's typing rules. I didn't say Haskell was up to that point. I don't think it is, for practical purposes. As for why you'd want to encode one language's typing rules in another language, one reason would be to prove the correctness of your type checker. The interesting question is how it works. But I suspect you have a misunderstanding of what I'm saying you could do. So you say intersection types require unification with expansion variables. Well what do you mean? Implementing type checking or type inference for intersection types requires it? Well who cares? We don't need to do either of those. We are encoding the type rules, and this doesn't entail dealing with algorithms at all. So before we talk about encoding type rules, you need to realize why the typing rules are not the same as an implementation of the type system. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
