search

vmware / differential-datalog

DDlog is a programming language for incremental computation. It is well suited for writing programs that continuously update their output in response to input changes. A DDlog programmer does not write incremental algorithms; instead they specify the desired input-output mapping in a declarative manner.
MIT License
1.38k stars 119 forks source link

Lift the "field must have the same type in all constructors" restriction [was: Field name conflict bug in Enum]. #994

Open qishen opened 3 years ago

qishen commented 3 years ago

I'm trying to define a new type that could be either string or integer. My first try is to write typedef NID = string | u32 but apparently not supported by ddlog so I came up with this one typedef NID = StrId {nid: string} | NumId {nid: u32}. The error message I got is error: graph.dl:10.15-11.1: Field nid is declared with different types saying the StrId and NumId cannot have the same field but it does not make sense since they are different constructors.

It could be a bug in the compiler and I also wonder what's the best way to write a union type that represents the union of multiple primitive types?

The other similar question is how to reuse the types defined in the relations if I want a union type like typedef Item = Node | Edge where input relation Node(id: u32) input relation Edge(src: Node, dst: Node)

ryzhyk commented 3 years ago

Ddlog requires that fields with different types in different constructors have different names.

ryzhyk commented 3 years ago

For the other question,

typedef Item = ItemNode{node: Node} | ItemEdge{edge: Edge}

Apologies about brevity and poor formatting. Typing on the phone.

ryzhyk commented 3 years ago

Ddlog requires that fields with different types in different constructors have different names.

By the way, this restriction was borrowed from Haskell and may not actually be necessary in ddlog. We may get rid of it in the future.

qishen commented 3 years ago

Thanks for answering me on your phone! I still don't have time (mainly because of procrastination) to look at Compile.hs and make changes for the previous PR yet but will try to figure it out and maybe help to remove this field name restriction too.

ryzhyk commented 3 years ago

I was hoping we'd convinced you to use ddlog instead of its internals :). There's unfortunately way too much on my to-do list to help with that feature in the near future.

As for the field name restriction, it's not just a matter of removing the check. We should also make sure it doesn't break type inference or any other part of the compiler, add tests for it, etc.

qishen commented 3 years ago

@ryzhyk You are very close to convincing me to use ddlog directly. I tried my own implementation built upon internals but does not work well. I'm still exploring the potential of ddlog to suit my needs in FORMULA and figure out if they have the exact same semantics despite using the same or similar syntax. One of the great things FORMULA has is nested aggregation (aggregation when certain constraints are satisfied but those constraints also have aggregation inside them) even though it's not used very often. The aggregation in ddlog seems to be highly customizable and I'll do more experiments on it.

If you can't beat 'em, join 'em

Maybe at the end I can just add a feature to ddlog if the feature I need does not exist or a wrapper on top of ddlog. We will see.

Do you guys have a slack channel for ddlog users?

ryzhyk commented 3 years ago

There's a gitter link in the readme. Or feel free to use the discussions section on GitHub.