On Mon, Jun 1, 2015 at 12:09 PM, Jonathan S. Shapiro <s...@eros-os.org> wrote:
> On Sun, May 31, 2015 at 11:23 AM, Matt Oliveri <atma...@gmail.com> wrote:
>> On Sun, May 31, 2015 at 10:51 AM, Jonathan S. Shapiro <s...@eros-os.org>
>> wrote:
>>
>> > So first, many of these languages actually don't have a way to define
>> > mutually recursive types.
>>
>> I don't believe you. :) The only popular language I know of that
>> doesn't effectively have mutually recursive types is SQL, which of
>> course doesn't have recursion at all.

(I've been informed that SQL does have recursion. So maybe you
technically could imitate mutual recursive types in SQL if you're
crazy enough.)

> So first, I mis-wrote that. I meant to write "co-recursive" as opposed to
> "mutually recursive".

Oh! I'm sorry, I assumed you meant mutually recursive all along. I
don't see what corecursion has to do with any of this.

> But I stand by what I said. There are, for example, no
> mutually recursive types in Java, C, C#, or (so far as I know) Haskell or
> OCaml.
>
> In all of these languages, it is possible to forward-declare a type in some
> fashion and then use *references* to the forward-declared type before the
> type itself is declared/defined.
>
> That's not a mutually recursive type.

I don't see forward references as fundamentally different from
recursive definitions, since that's exactly what they let you do. This
seems like just a difference in syntax. So, in particular, I'd say
Java, C, C#, Haskell, and OCaml all definitely have mutually recursive
types.

But anyway, I don't think OCaml allows arbitrary forward references,
or has forward declarations. The syntax for mutually recursive types
is:
type foo =
  ...
and bar =
  ...

With this syntax, foo can refer to bar.

>> > Second, merely factoring out the common fields isn't the goal here. The
>> > goal is to do that in such a way that we end up with a type
>> > that can describe the kind of AST that is typically associated
>> > with a context-free grammar.
>>
>> Right. I think that context-free-ness is what makes it possible, even
>> if it turns out to be too bulky or messy. With context-sensitive,
>> you'd need dependent types. (Or just GADTs, if you're lucky.)
>
> Perhaps. And I think there's a point at which you say "I've encoded enough
> in types to get most of the value I'm going to get out of checking, and it's
> time to stop".

Well I could point out here that if the end goal is correctness
proofs, just testing the particular ASTs you encounter at runtime is
not going to be enough. But I know your end goal is not correctness
proofs.

> But I don't even see a good solution for CFGs, because of the "subunion"
> issue. I know how to deal with that using dynamic checks, but not
> statically.

I guess I don't see why subunions are important for ASTs for CFGs. It
seems to me like unions of unboxed tuples are good enough. Subunions
would additionally guarantee the use of the same tag for the same leg
in all subunions of a given union. But why is that so important? And
of course, those unboxed tuples being unboxed is an optimization. It
still works if they're boxed.
_______________________________________________
bitc-dev mailing list
bitc-dev@coyotos.org
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to