miking-lang / miking

Miking - the meta viking: a meta-language system for creating embedded languages
Other
51 stars 31 forks source link

Type definitions in language fragments are not ordered correctly #570

Open dlunde opened 2 years ago

dlunde commented 2 years ago

The program

...

lang Align = MExprPPLCFA

  type AlignFlow = {
    unaligned: [Name],
    lhss: [Name]
  }

  type AlignAcc = {
    mMap: Map Name AlignFlow, <-- Type error points here, it doesn't look like the above definition of AlignFlow is visible here
    lMap: Map Name AlignFlow,
    current: AlignFlow
  }

  ...

gives the type error

FILE "miking-dppl/coreppl/align.mc" 198:19-198:28 ERROR: Unknown type constructor in symbolizeExpr: Align_AlignFlow

@larshum looked into this and wrote the following:

The error is that the aliases (in the lang_data) are stored in a map (the Record.t type is a map with ustring keys), so the order in which they were declared is not respected. I tried replacing it with an associative list, but this led to a stack overflow when bootstrapping (it’s also a really bad idea since merging will take O(n^2) time).

lingmar commented 2 years ago

Maybe related: syns can escape their language fragment and be used in top-level type declarations:

type MyType = MySyn

lang MyLang
  syn MySyn =
  | Syn {}
end

mexpr
use MyLang in
let s: MyType = Syn {} in
()

This program passes the type checking, and the pure MExpr code looks like this:

$ mi compile --test --keep-dead-code --typecheck --debug-parse temp.mc

type MySyn =
  <>
in
type MyType =
  MySyn
in
con MyLang_Syn: (()) -> (MySyn) in
let s: MyType =
  MyLang_Syn
    {}
in
{}
elegios commented 2 years ago

I found the source of the "syns escaping their fragment" issue: https://github.com/miking-lang/miking/blob/4ccffe8e9775f384696416ffe53582581888f8aa/src/boot/lib/mlang.ml#L933-L942

We just insert all syn types at the beginning of the program and do no mangling, whereby the early uses end up ok. In general this means that all syn types are global, and (probably?) always shadowed by other types. I suspect that's not the semantics we'd ideally want, but it's easier than something more proper, and I don't think we've quite specified what the semantics should be.

I suspect the whole mlang thing could use a bit of an overhaul with what we've learned, but probably better to do that when we go towards full selfhosting.