What's wrong with this function?

[emum]

(tc +)
(datatype color
    if (element? Color ["blue" "yellow"
                        "green" "grey"
                        "black" "orange"])
    ________________________________________
    Color : color;
)
(define check-o
{color --> boolean}
    Tocheck -> (== (hdstr Tocheck) "o")
)

This loads fine and individually (== (hdstr "oo") "o") does work and returns a boolean, however (check-o "orange") gives me a type error. Why please?

[Mark Tarver]

An interesting example.    There is a distinction from the early Wittgenstein between showing and saying.

For example,  I can see that your color datatype shows me that the longest inhabitant has six characters.

However your rule does not say that  the longest inhabitant has six characters.

Your rule shows me that colors are string.

But it does not state that colors are strings.

A type checker only functions with what is said and not what is shown.   hdstr expects a string and cannot infer

it receives one.  Hence the error.

Mark

[emum]

Ok, makes sense. Can you point me in the right direction how to fix? I also tried

(datatype color

if (element? Color ["blue" "yellow"

"green" "grey"

"black" "orange"])

Color : string;

=======================================

Color : color;)

so now I'm explicitly saying that Color must be a string, correct? but still getting "type error in rule 1 of check-o" trying to load.

[Mark Tarver]

The rule you have given entails 

if (element? Color ["blue" "yellow" "green" "grey" "black" "orange"])

Color : string >> P;

________________

Color : color >> P;

But the side condition is preventing the inference you need.  ToCheck is a variable which is not an element in the list cited.

You need to say that any assumption to the effect that Color is a color can be replaced by the assumption that Color is a string.

(datatype color

if (element? Color ["blue" "yellow" "green" "grey" "black" "orange"])

_________________________
Color : color;

Color : string >> P;
_____________________
Color : color >> P;)

Mark

Mark

--
You received this message because you are subscribed to a topic in the Google Groups "Shen" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/qilang/9-6zAAJ8E_U/unsubscribe.
To unsubscribe from this group and all its topics, send an email to qilang+un...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/qilang/3ce8bdf6-9641-451d-b38e-4da41dcb8affn%40googlegroups.com.

[Bruno Deferrari]

Hi emum, you may find this document that Neal wrote useful: https://github.com/Shen-Language/wiki/wiki/Sequent-Calculus

In particular, the "IV. Assumption Context" section, it may help you to better understand what Mark just showed you.

You received this message because you are subscribed to the Google Groups "Shen" group.
To unsubscribe from this group and stop receiving emails from it, send an email to qilang+un...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/qilang/CAGp%3DqtRdZxGBc%2BxMyQL%3DoEdmjhycLPuZex6WYVw%3DO%2BNC6bxXjg%40mail.gmail.com.

--

BD

[emum]

Appreciate it! Thank you both. Will mull this over.

Related — Dr. Tarver, you mentioned there was a new edition of LP&C coming? No rush, but is there an eta on that one?

[emum]

And also unrelated — How do you use \+ and fail in shen prolog? I'm checking the shen doc but it doesn't have it. Are these exposed to the developer?

[Mark Tarver]

(0-) (defprolog neg
      P <-- (call P) ! (when false);
      _ <--;)
(fn neg)

(1-) (prolog? (neg (mortal socrates)))
fn: mortal is undefined

(2-) (defprolog mortal
       plato <--;)
(fn mortal)

(3-) (prolog? (neg (mortal socrates)))
true

(4-) (prolog? (neg (mortal plato)))
false

Mark

On Sat, May 7, 2022 at 11:30 PM emum <emum...@gmail.com> wrote:

And also unrelated — How do you use \+ and fail in shen prolog? I'm checking the shen doc but it doesn't have it. Are these exposed to the developer?

--

You received this message because you are subscribed to the Google Groups "Shen" group.
To unsubscribe from this group and stop receiving emails from it, send an email to qilang+un...@googlegroups.com.

To view this discussion on the web, visit https://groups.google.com/d/msgid/qilang/cc5ba548-5fc0-4d7e-ac0e-fde474021413n%40googlegroups.com.

[emum]

Just wanted to add an fyi; not sure if this is an unknown issue or expected:

I tried implementing this solution for length/2/3 which works in swipl in shen prolog

swipl

pllen(Xs,L) :-
    pllen(Xs,0,L).
pllen([],L,L).
pllen([_|Xs],T,L) :-
  T1 is T+1,
  pllen(Xs,T1,L).

shen

(defprolog pllen

Xs L <-- (pllen Xs 0 L);

[] L L <--;

[_ | Xs] T L <--

(is T1 (+ T 1))

(pllen Xs T1 L);)

and I get "arity error in prolog procedure pllen" so I guess it has a problem with the parametric polymorphism? Is this expected for the Edinburgh implementation?

[Mark Tarver]

About your fork - maybe a bug.  But this is a simple arity error pllen has arities 2 (RULE 1) and arities 3 elsewhere.

M.

[Mark Tarver]

This isn't really parametric polymorphism but polyadicity.  In logic a relation should have a fixed number of terms and in 

ATPS like Prover9, you cannot have f(a) and f(b,c).   Shen Prolog follows suit here.  SWI Prolog lets you get away with it.

But Shen Prolog is not an ISO Prolog nor was intended to be.  I don't know what the ISO standard is here.

Mark

On Sunday, 8 May 2022 at 22:29:04 UTC+1 emum wrote: