On 12 Jun 2015 1:25 pm, "Matt Oliveri" <[email protected]> wrote: > > 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.
Yes, I think you are right. I don't quite get the distinction. Let's say the target language has binary numeric operators on floats and ints implemented as intersection types, such that: + : Int -> Int -> Int /\ Float -> Float -> Float Obviously when parsing a subterm of the operator, let's just consider literals for now, we would require both to be Float or Int. How could we ensure such expressions are well formed in a host language that does not have intersection types? Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
