LogicList type needed

[acfoltzer]

Like in previous incarnations of this system, we need an alternative to the built-in list type:

data [a] = [] | a : [a]

This isn't suitable for our purposes, since we don't necessarily have a tail that's actually a list, but the : constructor requires one. Instead, we need a list that's more like this:

data [a] = [] | a : (LogicVar [a])

This type would rule out improper lists, since the ground value for the tail, if any, is another list. However, we can't yet overload the []/: syntax, so it'll probably have to be something awkward like:

data LogicList a = Nil | Cons a (LogicVar (LogicList a))

Does this type sound good? Once we decide on it, we should provide an alternative Data.List module, although it remains to be seen how higher-order combinators might behave in this setting.

[dfried00]

I think it is a reasonable first attempt, but what will it do with Oleg
Numbers and
reification in general.

... Dan

On Sun, Jan 29, 2012 at 3:13 PM, Adam Foltzer <
[email protected]

wrote:

Like in previous incarnations of this system, we need an alternative to
the built-in list type:

data [a] = [] | a : [a]

This isn't suitable for our purposes, since we don't necessarily have a
tail that's actually a list, but the : constructor requires one. Instead,
we need a list that's more like this:

data [a] = [] | a : (LogicVar [a])

This type would rule out improper lists, since the ground value for the
tail, if any, is another list. However, we can't yet overload the []/:
syntax, so it'll probably have to be something awkward like:

data LogicList a = Nil | Cons a (LogicVar (LogicList a))

Does this type sound good? Once we decide on it, we should provide an
alternative Data.List module, although it remains to be seen how
higher-order combinators might behave in this setting.

---

Reply to this email directly or view it on GitHub:
https://github.com/acfoltzer/typed-logic-programming/issues/1

[acfoltzer]

Well, Oleg Numbers are isomorphic to LogicList Bool, so if we can do one, we should have the other.

Reification (and unification) are a pain to define right now with lots of boilerplate, but there are generic programming techniques to address this. Now that we've escaped from the tyranny of the all-encompassing sum type for values, though, it should be mostly straightforward, although there will be interesting problems with recursively-defined types.

[dfried00]

There is a paper called "Typed Logic Variables" that you should look at.
If you can't find it, the author's last name is Classen or Claussen.

... Dan

On Sun, Jan 29, 2012 at 3:25 PM, Adam Foltzer <
[email protected]

wrote:

Well, Oleg Numbers are isomorphic to LogicList Bool, so if we can do
one, we should have the other.

Reification (and unification) are a pain to define right now with lots of
boilerplate, but there are generic programming techniques to address this.
Now that we've escaped from the tyranny of the all-encompassing sum type
for values, though, it should be mostly straightforward, although there
will be interesting problems with recursively-defined types.

---

Reply to this email directly or view it on GitHub:

https://github.com/acfoltzer/typed-logic-programming/issues/1#issuecomment-3710936