[ANN] S34 kernel

[Mark Tarver]

The S34 kernel is available for download.  This fixes the compiler bug reported by Neal four days ago and incorporates assert and retract for Shen Prolog.  A documentary summary

of the latter is provided here.

I'll be upgrading SP to S34 very soon.

Mark 

[nha...@gmail.com]

Yacc fails if there are variables in the result type. I think this is due to the 'type' annotations that get generated, and the fact that 'type' doesn't handle variables properly.

(defcc <test>
  { (list number) ==> (list A) }
  1 := [];)

It complains about free variable A, but even if you suppress the free variable check it doesn't work right because (type X (list A)) doesn't have the same symbol value for 'A' when unifying the type signature and type annotation (it tries: A = &&&A).

[Mark Tarver]

Basically the type annotation was done to offset some of the 

overheads of type checking YACC code.  But the new algorithm should make these

annotations unnecessary.

M.

[nha...@gmail.com]

Besides YACC not needing the type annotations anymore, 'type' still can't reference type variables in the signature.

This patch below fixes it:

(package shen [&]
 (defprolog t*
   (- [define F | X]) A <-- !
                            (bind SigxRules (sigxrules [(0 F) | (0 X)]))
                            (bind Sig (fst (1 SigxRules)))
                            (bind Rules (snd (1 SigxRules)))
                            (bind Assoc (type-mapping Sig))
                            (bind FreshSig   (freshen-type Assoc Sig))
                            (bind FreshRules (freshen-rules Assoc Rules))
                            (t*-rules F FreshRules FreshSig 1)
                            (is Sig A);)

 (define type-mapping
   Sig -> (let Vs (extract-vars Sig)
             (map (/. V [V | (freshterm (concat & V))]) Vs)))

 (define freshen-rules
   Assoc [type X T] -> [type (freshen-rules Assoc X)
                             (freshen-type Assoc T)]

   Assoc (@p L R) -> (@p (freshen-rules Assoc L)
                         (freshen-rules Assoc R))

   Assoc XS -> (map (/. X (freshen-rules Assoc X)) XS)
     where (cons? XS)

   Assoc X -> X)



(define find-free-vars
  Bound [type X T] -> (find-free-vars Bound X)
  Bound [protect V] -> []
  Bound [let X Y Z] -> (union (find-free-vars Bound Y) (find-free-vars [X | Bound] Z))
  Bound [lambda X Y] -> (find-free-vars [X | Bound] Y)
  Bound [X | Y] -> (union (find-free-vars Bound X) (find-free-vars Bound Y))
  Bound V -> [V]    where (free-variable? V Bound)
  _ _ -> [])
)

[Mark Tarver]

My thoughts on this were interrupted by Covid at a time when I was just beginning an experimental implementation.

As regards the implementation, automatic type annotations were only included to optimise the speed of type checking (not

to change the result) and could be dropped in these polymorphic cases without really showing much noticeable effect on the 

system as a whole.  The typechecker can find its own way there without misdirection.  The simplest fix is to avoid misdirecting

automatic type annotations and this is easily done.  

Having gone a bit deeper into the issue of the nature of ==> I've come to the conclusion that TBoS got it right in not making it primitive

because the effect of doing so has ramifications that are problematic.  In particular YACC functions are always applied in the context

of the higher-order compile function as in (compile (fn <mycompiler>)  something-or-other).  The fn part is needed and then we are

in deep waters.  fn is a shorthand for a lambda construction which in turn expands to (/. X (<mycompiler> X)) and the Rule of Applications

requires that <mycompiler> have the type (A --> B) for some A and B.   Of course under the "==> is primitive" school it does not and so we are

faced with a major revision at the level of typed lambda calculus and this is definitely Not a Good Thing.

So TBOS made the right decision in making ==> syntactic sugar and leaving logical theory untouched and evolving an approach 

that plugs into the existing theory and type checker.

Now as regards your implementation and the 3,000,000 inferences needed to certify the system; this is larger than I experienced

with a compiler for a subset of C (80,356 inferences for 515 lines of code).  I think that this is probably a function of your type

theory rather than YACC and probably the fact that you are effectively defining the type of all symbolic expressions (from memory

of your program).  I cannot run your program to see what is going on because you are using bespoke constructions.   But from

experience the type of symbolic expressions often leads to exponential blowups.  For example the expression [a b c] is a 

symbolic expression but it is also a list of symbolic expressions.

Hence because of this type ambiguity, the type checker can assign a symbolic expression the wrong type and have to unpick this

decision later in the proof search.  It is effectively working with a binary tree in terms of search and exponential blowups are common.

I'm not altogether unsurpised that you have a heavy overhead even though the speed of the typechecker under Scheme on my

computer would dispose of this in 1.5 seconds.  It isn't a YACC problem specifically, but a problem with working with this particualr

type.

I'll put up a fix for misdirected type annotations which should not be hard.

Mark

[Mark Tarver]

Shen, www.shenlanguage.org, copyright (C) 2010-2022, Mark Tarver
version: S34.2, language: Common Lisp, platform: SBCL 2.0.0
port 3.2, ported by Mark Tarver


(0-) (tc +)
true

(1+) (defcc <f>
       {(list symbol) ==> (list A)}
        a := [];)
(fn <f>) : ((list symbol) ==> (list A))

Seems to be fine.  I'll put this up.

Mark

[Mark Tarver]

This has been patched over the cloud in SP.

Mark