On Fri, Jun 12, 2015 at 8:32 AM, Keean Schupke <[email protected]> wrote:
> 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:
>> > 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.
>>
>> 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.
You were doing great until you said "parsing". We want to separate
that from the encoding of the typing rules, just like we do on paper.
> How could we ensure such expressions are well formed in a host language that
> does not have intersection types?
That's the question alright. First of all, we want types for ASTs. One
for value-level expressions ("terms"), one for type expressions. Then
we can define a type of typing contexts to be lists of type
expressions. (I'm a de Bruijn index buff. Screw the variable names.)
Then we define the typing rules as an inductive relation on a context,
term and type expression.
That's probably the most low-tech way to do it. It might even work in
Prolog. It's basically like on paper. Just the notation is different.
Proof assistants make this very easy. Well actually, handling the
variables is a PITA.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
