A compiler error on Unification.hs when accessing the field

[qishen]

I got a compiler error if I uncomment var node = reversed_list.node in the function nonnull_list_nth() to access the field. I don't quite understand the error message: ddlog: Unification.teToType: non-constant type expression 'a50 CallStack (from HasCallStack): error, called at src/Language/DifferentialDatalog/Unification.hs:415:35 in differential-datalog-0.42.0-1PgGWEVSzEkJuq6cM15JM0:Language.DifferentialDatalog.Unification. Hope I find another bug to improve ddlog or let me know the right way to write the function in my linked list implementation. Thanks!

function into_nonnull_vec(list: mut NonNullList<'N>): Vec<'N> {
	// Have to reverse the list first because `Vec<T>` does not support insertion
	// at the beginning of the vector
	var reversed_list = nonnull_list_reverse(list);
	// var node = reversed_list.node;
        // FIXME: A ugly workarond to please the compiler
	var node = nonnull_list_nth(reversed_list, 0).unwrap_or_default();
	var nxt = nonnull_list_nxt(reversed_list);
	// match (reversed_list.nxt) {
	match (nxt) {
		NonNullNxt { nxt_nonnull_list_ref } -> {
			var nxt_nonnull_list = deref(nxt_nonnull_list_ref);
			var vector = into_nonnull_vec(nxt_nonnull_list);
			vec_push(vector, node);
			vector
		},
		NULL -> {
			var vector = vec_empty();
			vec_push(vector, node);
			vector
		}
	}
}

Below is a quick implementation of linked list in DDLog that probably has the worst performance on list operations because of tons of deref() and ugly workarounds but I'm using this linked list implementation somewhere that does not require high performance or even incrementality. I appreciate any suggestion to enhance it even though you may not want it to be included in the standard library.

// The `NonNullList` must have at least one item in the list and can't be null
// `NonNullList` in Formula representation:
// LinkedList ::= new (node: N, nxt: LinkedList + NULL)
typedef NonNullList<'N> = NonNullList { node: 'N, nxt: NonNullNxt<'N> }
typedef NonNullNxt<'N> = NonNullNxt { nxt: Ref<NonNullList<'N>> } | NULL

function from_singleton_to_nonnull_list(item: 'N): NonNullList<'N> {
	NonNullList { item, NULL }
}

function from_nonnull_vec(vector: mut Vec<'N>): Option<NonNullList<'N>> {
	if (vec_len(vector) == 0) {
		None
	} else {
		var last = vector.pop().unwrap_or_default();
		var list_without_last_opt = from_nonnull_vec(vector);
		match (list_without_last_opt) {
			Some {list_without_last} -> {
				var nonnull_list = nonnull_list_append(list_without_last, last);
				Some { nonnull_list }
			},
			None -> { 
				Some { NonNullList { last, NULL } }
			}
		}
	}
}

function into_nonnull_vec(list: mut NonNullList<'N>): Vec<'N> {
	// Have to reverse the list first because `Vec<T>` does not support insertion
	// at the beginning of the vector
	var reversed_list = nonnull_list_reverse(list);
	// FIXME: A workarond to please the compiler
	// var node = reversed_list.node;
	var node = nonnull_list_nth(reversed_list, 0).unwrap_or_default();
	var nxt = nonnull_list_nxt(reversed_list);
	// match (reversed_list.nxt) {
	match (nxt) {
		NonNullNxt { nxt_nonnull_list_ref } -> {
			var nxt_nonnull_list = deref(nxt_nonnull_list_ref);
			var vector = into_nonnull_vec(nxt_nonnull_list);
			vec_push(vector, node);
			vector
		},
		NULL -> {
			var vector = vec_empty();
			vec_push(vector, node);
			vector
		}
	}
}

// A helper function for the temporary workaroud
function nonnull_list_nxt(list: NonNullList<'N>): NonNullNxt<'N> {
	list.nxt
}

function nonnull_list_nth(list: NonNullList<'N>, i: usize): Option<'N> {
	if (i == 0) {
		Some{ list.node }
	} else {
		match (list.nxt) {
			NonNullNxt { nxt_nonnull_list_ref } -> {
				var nxt_nonnull_list = deref(nxt_nonnull_list_ref);
				nonnull_list_nth(nxt_nonnull_list, i-1)
			},
			NULL -> { None }
		}
	}
}

function nonnull_list_append(list: mut NonNullList<'N>, item: 'N): NonNullList<'N> {
	match (list.nxt) {
		NonNullNxt { nxt_nonnull_list_ref } -> {
			var nxt_nonnull_list = deref(nxt_nonnull_list_ref);
			var nxt_nonnull_list_with_item = nonnull_list_append(nxt_nonnull_list, item);
			nxt_nonnull_list_with_item
		},
		NULL -> { 
			// Create a NonNullList with two items
			var nxt = NonNullNxt { ref_new(NonNullList { item, NULL }) };
			NonNullList { list.node, nxt }
		}
	}
}

function nonnull_list_reverse(list: mut NonNullList<'N>): NonNullList<'N> {
	match (list.nxt) {
		NonNullNxt { nxt_nonnull_list_ref } -> {
			var nxt_nonnull_list = deref(nxt_nonnull_list_ref);
			var reversed_nxt_nonnull_list = nonnull_list_reverse(nxt_nonnull_list);
			nonnull_list_append(reversed_nxt_nonnull_list, list.node)
		},
		NULL -> { list }
	}
}

function nonnull_list_map(list: NonNullList<'N>, f: function('N): 'M): NonNullList<'M> {
	var new_node = f(list.node);
	var mapped_nonnull_nxt = match (list.nxt) {
		NonNullNxt {nxt_nonnull_list_ref} -> {
			var nxt_nonnull_list = deref(nxt_nonnull_list_ref);
			var mapped_nonnull_list = nonnull_list_map(nxt_nonnull_list, f);
			NonNullNxt { ref_new(mapped_nonnull_list) }
		},
		NULL -> NULL
	};
	NonNullList { 
		new_node, 
		mapped_nonnull_nxt
	}
}

// `List` in Formula representation:
// NonNullLinkedList ::= new (node: N, nxt: LinkedList)
// LinkedList ::= NonNullLinkedList + NULL 
typedef List<'N> = List { node: 'N, nxt: ListNxt<'N> } | EMPTY
typedef ListNxt<'N> = ListNxt { nxt: Ref<List<'N>> }

function from_singleton_to_list(item: 'N): List<'N> {
	List { item, ListNxt {ref_new(EMPTY)} }
}

function from_vec(vector: mut Vec<'N>): List<'N> {
	if (vec_len(vector) == 0) {
		EMPTY
	} else {
		var last = vector.pop().unwrap_or_default();
		var list_without_last = from_vec(vector);
		list_append(list_without_last, last)
	}
}

function into_vec(list: mut List<'N>): Vec<'N> {
	var reversed_list = list_reverse(list);
	match (reversed_list) {
		List { node, ListNxt {nxt_list_ref} } -> {
			var nxt_list = deref(nxt_list_ref);
			var inner_vec = into_vec(nxt_list);
			vec_push(inner_vec, node);
			inner_vec
		},
		EMPTY -> { vec_empty() }
	}
}

function list_nth(list: List<'N>, i: usize): Option<'N> {
	match (list) {
		List { node, ListNxt {nxt_list_ref} } -> {
			if (i == 0) { Some {node} } 
			else {
				var nxt_list = deref(nxt_list_ref);
				list_nth(nxt_list, i-1)
			}
		},
		EMPTY -> { None }
	}
}

// Since `Ref<List<'N>>` is immutable we have to make a deep copy and append the new item
function list_append(list: mut List<'N>, item: 'N): List<'N> {
	match (list) {
		List { node, ListNxt { nxt_list_ref } } -> {
			var nxt_list = deref(nxt_list_ref);
			var nxt_list_with_item = list_append(nxt_list, item);
			List { node, ListNxt { ref_new(nxt_list_with_item) } }
		},
		EMPTY -> {
			List { item, ListNxt { ref_new(EMPTY) } }
		}
	}
}

function list_reverse(list: mut List<'N>): List<'N> {
	match (list) {
		List { node, ListNxt {nxt_list_ref} } -> {
			// TODO: Deref literally on every iteration is bad.
			var nxt_list = deref(nxt_list_ref);
			var reversed_nxt_list = list_reverse(nxt_list);
			list_append(reversed_nxt_list, node)
		},
		EMPTY -> EMPTY
	}
}

function list_map(list: List<'N>, f: function('N): 'M): List<'M> {
    match (list) {
		List { node, ListNxt {nxt_list_ref} } -> {
			var nxt_list = deref(nxt_list_ref);
			var mapped_nxt_list = list_map(nxt_list, f);
			List { f(node), ListNxt {ref_new(mapped_nxt_list)} }
		},
		EMPTY -> EMPTY
    }
}

[ryzhyk]

This is certainly a bug, I'll look into it.

[qishen]

A quick question that is not really related to this issue: Why does an expression like p in Path[Path{u, u}] requires every variable in it to be unique?

[mihaibudiu]

This is #197

[ryzhyk]

@qishen, I believe I fixed the bug in my fork. I will submit a PR with the fix shortly, I just want to also add your linked list example as a test, but haven't had a chance to go through it yet. Do you happen to have some code/data to test your implementation?

[qishen]

@ryzhyk Sorry I haven't tested my implementation yet and just use the linked list in a few places assuming the implementation is correct. I can help to write some tests on the linked list if you want.

[ryzhyk]

Comments regarding list implementation:

• I think you could replace NonNullNxt<'N> with Option<Ref<NonNullList<'N>>>.
• from_nonnull_vec - I don't think a recursive implementation is a good idea. I would rather use a for-loop to iterate over the vector. This way you won't have to destroy the input vector.
• into_nonnull_vec - as an alternative to reversing the list, you could preallocate the vector using vec_with_length and use
  update_nth to update elements starting from the end of the vector. This would require a length(List) function.
• nonnull_list_reverse is unnecessarily expensive as it scans the list on each recursive call
• There are a bunch of functions where arguments are declared as mut, but they don't need to be.
• Since constructors live in the global namespace, names like NULL, EMPTY are likely to cause conflicts.

Looks ok otherwise, but also kind of shows that ddlog is not the best language for implementing these data structures right now. A native implementation in Rust would probably work better (and would enable double-linked lists as well).

[ryzhyk]

nonnull_list_append is incorrect. Here is a correct implementation:

function nonnull_list_append(list: NonNullList<'N>, item: 'N): NonNullList<'N> {
	match (list.nxt) {
		NonNullNxt { nxt_nonnull_list_ref } -> {
			var nxt_nonnull_list = deref(nxt_nonnull_list_ref);
			NonNullList { list.node, NonNullNxt { ref_new(nonnull_list_append(nxt_nonnull_list, item)) } }
		},
		NULL -> { 
			// Create a NonNullList with two items
			var nxt = NonNullNxt { ref_new(NonNullList { item, NULL }) };
			NonNullList { list.node, nxt }
		}
	}
}

[ryzhyk]

into_nonnull_vec is also incorrect because it reverses the vector on each recursive call, and not just initially.

This seems to work:

function length(list: NonNullList<'N>): usize {
    match (list.nxt) {
        NULL -> 1,
        NonNullNxt{nxt} -> 1 + nxt.deref().length()
    }
}

function into_nonnull_vec(list: NonNullList<'N>): Vec<'N> {
    var res = vec_with_capacity(list.length());
    into_nonnull_vec_inner(list, res);
    res
}

function into_nonnull_vec_inner(list: NonNullList<'N>, vec: mut Vec<'N>) {
    vec.push(list.node);
    match (list.nxt) {
        NULL -> (),
        NonNullNxt{nxt} -> into_nonnull_vec_inner(nxt.deref(), vec)
    }
}

[ryzhyk]

A better implementation of from_nonnull_vec (I will create a PR with Vec::reverse_imm library function shortly):

function from_nonnull_vec(vector: Vec<'N>): Option<NonNullList<'N>> {
    var res = None;

    for (v in vector.reverse_imm()) {
        match (res) {
            None -> {
                res = Some{NonNullList{ v, NULL}}
            },
            Some{list} -> {
                res = Some{NonNullList{v, NonNullNxt{ref_new(list)}}}
            }
        }        
    };
    res
}

[qishen]

Thanks and I just found the same issues when testing it on some real data.