Environments, side channels and state

[nha...@gmail.com]

It's unclear what the best approach for this is in Shen.

Haskell offers Reader, Writer and State monads for this, but it is not really an appealing approach in Shen. It ends up being quite invasive even with macros, since part of the convenience of their use in Haskell relates to type classes, which is in part implemented via dynamic binding (implicit parameters). Most Shen backends won't be able to inline the monadic bind operator as well, which may lead to performance issues. Furthermore monads are actually overkill for this use case because the control flow capabilities of their underlying CPS-like nature is unused.

Another newer alternative is Algebraic Effects, but I think this requires a CPS transform, which is also highly invasive relative to the simplicity of what were looking for.

Lisp style dynamic binding really seems like the simplest solution, especially since Shen doesn't have call/cc.

 

A typed example implementation is here:

https://github.com/NHALX/shen-misc/blob/master/env.shen

https://github.com/NHALX/shen-misc/blob/master/misc.shen

Which implements fluid-let, sow/reap (https://reference.wolfram.com/language/ref/Reap.html) and basic state.

The environment has to be passed in as a parameter, because T* is a bit restrictive with function definitions, but this may have some benefits vs having it be in a thread local or global variable.

An environment (hash table) is given a type like:

(env *index*  : r (list number)
     *inline* : r (substitutions A (list number) A)
     *rename* : r (substitutions A unit B)
     *recur*  : r (forall a (forall b ((foil a) --> (foil b)))))

Which is a bit like an assumption context reified into a type, so the order of the type annotations shouldn't matter, and subsets of the environment are inferred when needed.

Using lazy evaluation you can evaluate a thunk in a given dynamic binding environment:

(define test3
  { (env *test2* : r number) --> (lazy number) --> number }

  Env X -> (let! Env
               *test* 1
               *test2* (+ 1 *test*)
             (thaw X)))


(let Env (env-new)
   (fluid-let Env
              *test2* 0
              (freeze (test3 Env (freeze (fluid-value Env *test2* ))))))

The rules for fluid-let are:

(datatype @env-let@

                     Env : (env | Have) >> Value : A;
                       (update Key r A Have Have*);
                 Env : (env | Have*) >> Body : (lazy C);
       _________________________________________________________
       Env : (env | Have) >> (fluid-let Env Key Value Body) : C;

                           (env? Key r A Have);
         ______________________________________________________
             Env : (env | Have) >> (fluid-value Env Key) : A;   )

(datatype @env-update@

               if (and (== Key K) (== Domain D))
                              !;
            (unify (Key : Domain Value | XS) Tail);
    _______________________________________________________
      (- (update Key Domain Value (K : D _ | XS) Tail));

               (update Key Domain Value XS XS*);
                 (unify (K : D V | XS*) Tail);
       _________________________________________________
      (- (update Key Domain Value (K : D V | XS) Tail));

                              !;
              (unify (Key : Domain Value) Tail);
       _________________________________________________
            (- (update Key Domain Value () Tail));

                               )

(define fl-query
  Key Domain [Key : Domain Value | XS] -> [just Value]
  Key Domain [_ : _ _ | XS] -> (fl-query Key Domain XS)
  _ _ _ -> nothing)

(datatype @env@


           let Query (fl-query Key Domain Set)
               (unify (just Type) Query);
        _________________________________________
              (env? Key Domain Type Set);

            ________________________________
                 (env-new) : (env);

                    (check-all B A);
    _________________________________________________
           X : (env | A) >> X : (env | B);

                            )

[nha...@gmail.com]

Because fl-query is a function, this doesn't typecheck:

(lambda E (@p (fluid-value E *key1*) (fluid-value E *key2*)))

You could do something like:

(datatype @env-contains?@
                              (unify XS ());
                            __________________
                                (seal XS);

                                (seal XS);
                         _______________________
                              (seal (X|XS));


                              (unify Key K);
                            (unify Domain D);
                                    !;
                             (unify Type V);
                                (seal XS);
    __________________________________________________________________
               (contains? Key Domain Type (K : D V | XS));

                     (contains? Key Domain Type XS);
    __________________________________________________________________
               (contains? Key Domain Type (K : D V | XS));   )

But this has bad backtracking behaviour and can go on forever. 

You could place a static limit on the size of the list to force termination, but is there any better way to deal with this?

[nha...@gmail.com]

Maybe sticking with fl-query and requiring a type annotation is better.

You tend not to need to use too many annotations if they are placed in a good spot, and something like this isn't too intrusive:

(lambda E (let E (type E (env *key1* : r A
                              *key2* : r B))

             (@p (fluid-value E *key1*)
                 (fluid-value E *key2*))))

[Mark Tarver]

Wow, that's a lot of work.  Perhaps you should circulate this outside the group, write a paper or do a blog, since you seem to have read deeply into this.

Well what I have to say is modest.  It seems that you want to concentrate on those aspects of Shen which are not 'pure'.   The reference to side channels escapes me a little because I can only find references to side channel attacks and I cannot see the connection.  

The first thing to ask is 'What is the problem with impure Shen?'.   Which is really a question that can be asked of any impure language.  Of course we can create pure languages by omitting all the things above but actually they are of little practical use.

I think the reason for language designers like purity is that it reflects logic and mathematics.   x = x is a basic logical principle; but (= (read) (read)) will fail in Shen (type 0 and then 1).  Similar examples can be constructed with functions that use global variables, destructive vector assignments, gensym, read operations on files, getting universal time and so on.  What you get when you subtract all these things is pure Shen.   This almost works like logic and maths but not quite.  I'll come to that.

What is the reason for the failure of these operations to reflect logic?  Is it to do with state as the invisible parameter?  Well, no.  I mean you could imagine a read operation set up to dynamically read signals coming from an electronic source 1,000 miles away.   The failure of one read operation to match the next is not due to state.

The invisible parameter is time.  The expression (= (read) (read)) is really (= (read t1) (read t2)) for times t1 and t2, and once your restore the invisible parameters the failure of  (= (read) (read)) goes.  Philosophers say that the grammatical form of (= (read) (read)) is not the same as the logical form.  Wittgenstein said that in a logically perfect language, grammatical form and logical form coincide.

So in an ideal functional language, where logical form and grammatical form coincide, there would be purity. 

And we can attain purity by restoring time. However in the form I described, it would be quite difficult to use it.  We would have  to have a clock which begins at login you would enter (read t) in your program for some value of t.  What happens if the clock has run past t?  Does your read operation hang or return an error?

Suppose you are reading from a file.  Suppose your read operation is outrun by the clock.  Does your read fail?  

Alternatively, suppose you set up your read so the clock does not outrun it.  Now it sits around idling waiting for a clock to strike which is inefficient.  Similar remarks apply to the other impure features.

Supposing you could get past that. would Shen be pure?  No, the expression (= (/. X X) (/. X X)) fails returning false.  So you have to change the type of the equality function to allow for only non-functional objects.   But if you could do all these things, you'd have a pure Shen.

But AFAIK, nobody has done anything like this and I'm not sure that anybody would want to use the result!

What does this Haskell tutorial say?

https://www.haskell.org/tutorial/io.html

The return function admits an ordinary value such as a boolean to the realm of I/O actions. What about the other direction? Can we invoke some I/O actions within an ordinary expression? For example, how can we say x + print y in an expression so that y is printed out as the expression evaluates? The answer is that we can't! It is not possible to sneak into the imperative universe while in the midst of purely functional code. Any value `infected' by the imperative world must be tagged as such. A function such as

f    ::  Int -> Int -> Int

absolutely cannot do any I/O since IO does not appear in the returned type. 

So the Haskell solution seems to be to quarantine IO.  This is not hard to do in Shen with a revision of your types.  Of course that doesn't make Haskell pure.   Any more than a priest who confines his activities to a bordello is chaste. Wearing a prophylactic does not make you celibate.

M.

[nha...@gmail.com]

I just meant side channel in a casual sense - basically sow/reap or the Writer monad.

Monads in Haskell are pure, it's just the IO monad that is a bit fake. For example the Reader (read only environment) monad just uses lambda to delay the input of the environment until later:

return :: a -> (r -> a) 

Return takes an 'A' and produces a thunk waiting for the environment 'R' at a later point. The monad bind operator just composes everything.

The State monad works similarly and the Writer monad just appends an extra log to the output of functions.

I agree Haskell isn't pure under the hood. Consider also that the runtime probably does a lot of mutation behind the scenes to memoize lazy thunks after they have been evaluated.  

There are also monads like the ST monad which performs real mutation, yet doesn't need to be in the IO monad, because the mutations are statically guaranteed to be localised and therefore the whole block is observationally pure to the outside. 

So if you ignore all these things and outliers like https://hackage.haskell.org/package/base-4.17.0.0/docs/System-IO-Unsafe.html then you can maybe say Haskell is observationally pure.

The environment type in the first post uses mutation so it is fragile. The types for dynamic binding probably only work as long as it is used single threaded and execution doesn't manage to skip the state restoration block somehow.

Capturing the environment object when assigned different types and mixing them in the same dynamic extent probably breaks things too and I'm not really sure what to do about that.

[nha...@gmail.com]

For example, this is wrong because it thinks the number two has type string:

(let Env (env-new)
   (fluid-let Env
              *test2* 0

              (freeze (let Broken (fluid-let Env *test2* "hi"
                                             (freeze (freeze (let Discard (type (fluid-value Env *test2*) string)
                                                                (do (output "discard(string) is ~A~%" Discard)
                                                                    1234)))))
                         (test3 Env Broken)))))

[nha...@gmail.com]

The environment type signature needs to be tied to the function type signature somehow.

So maybe the fluid-value API could be changed to inject it's value into a continuation and wrap the result in a dummy 'context' type:

Env : E;
F : (A --> B); \\ TODO: extract A from E
__________________________________________________
(fluid-value Env *symbol* F) : (context E B);

And then (fluid-let) can strip the 'context' type tag if it can typ check 'E' against the current state of the environment at that point.  

[nha...@gmail.com]

It's too annoying to tag things with fluid-value so an empty wrapper function at the top level works better: 'use'

(datatype @env-let@
                                    X : A;
                        ______________________________
                            X : (- (context E A));

                     Env : (env | Have) >> Value : A;
                       (update Key r A Have Have*);
               \\  Env : (env | Have*) >> Body : (lazy C);

           Env : (env | Have*) >> Body : (lazy (context Have* C));
    ______________________________________________________________________

       Env : (env | Have) >> (fluid-let Env Key Value Body) : C;

                           (env? Key r A Have);

      _________________________________________________________________
          Env : (env-activated | Have) >> (fluid-value Env Key) : A;


                     Env : (env-activated | E) >> F : B;
           _______________________________________________________
               Env : (env | E) >> (use Env F) : (context E B);

                                      )

The API is already starting to suck though, and it is starting to absorb some of the characteristics of Haskell's monads wrt type wrappers.

(define test3
  { (env) --> (lazy (context (*test2* : r number) number))
          --> number }

  Env X -> (fluid-let Env *test2* 1 X))

\\ This works

(let Env (env-new)
   (fluid-let Env
              *test2* 0

              (freeze (use Env (fluid-value Env *test2*)))))

\\ This now gets correctly rejected due to string != number

(let Env (env-new)
   (fluid-let Env
              *test2* 0
              (freeze (let Broken (fluid-let Env *test2* "hi"

                                             (freeze (freeze (use Env

                                                                  (let Discard (type (fluid-value Env *test2*) string)
                                                                     (do (output "discard(string) is ~A~%" Discard)

                                                                         1234)) ))))
                         (test3 Env Broken)))))

[Mark Tarver]

I think to begin to unravel this, we need a statement of intent.  I mean, what is it you want to achieve or what problem are you specifically aiming to solve?  The purity problem, is, I think, practically unsolvable.   

M.

--
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/Ufubur2qOFE/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/47bd7286-a111-461f-b23c-49901f10f9efn%40googlegroups.com.

[nha...@gmail.com]

"I mean, what is it you want to achieve or what problem are you specifically aiming to solve?"

Let's focus on typed dynamically scoped variables (https://prl.khoury.northeastern.edu/blog/2019/09/05/lexical-and-dynamic-scope/).

Basically fluid-let in Scheme and I think maybe defvar in Common Lisp.

I think I got it working ok now in a somewhat reasonable way. It changes how T* works but I wanted some of these features for other reasons in the past.

*************

Problem 1. T* only accepts basic type signatures.

*************

Stock T* starts type checking inside the rule body and you can't control anything before that. The modified T* now starts at the top of the define and is restructured to allow you to inject things into the hypothesis context. 

For example this function:

(define test4
  { context (*test2* : r number) (number --> number) }
  N -> (+ N (fluid-value *test2*)) )

Type checking starts here:

(spy +)
typechecking (fn test4)
____________________________________________________________ 16 inferences
?- (shen.intro test4 (shen.rules test4 (shen.rule (N) (+ N (fluid-value *test2*))))) : Var10

1. test4 : (context (*test2* : r number) (number --> number))

 
The user can add rules like so:

(datatype ctx
                  (dynamic (env | P)), F : Sig >> (shen.intro F Rules) : A;
    ___________________________________________________________________________
                 F : (context P Sig) >> (shen.intro F Rules) : A;


      ______________________________________________________________________
              (dynamic (env | P)), F : (context P (A --> B)) >> F : (A --> B);


                                Rules : (A --> B);
                  ______________________________________________
                    F : (A --> B) >> (shen.intro F Rules) : C; )

F gets converted to (A --> B) and some assumptions are added to the context.

***********

Problem 2. Dynamic Scope vs Lexical Scope contexts

***********

Freeze and Lambda introduce new dynamic scopes, but the hypothesis list mostly just reflects the lexical state of things. Assumptions related to the current dynamic environment need to be reset inside a lambda because this environment won't be valid when the lambda is applied (they aren't allowed to capture any dynamic scope from the current lexical context).

Sequent calculus allows multiple context lists like gamma delta etc. We've talked about this before, but it would come in useful here to have a separate list for assumptions related to the dynamic scope.

That is a larger change though and I'll save it for later. For now, the second list is being simulated by tagging certain list entries with (dynamic).

The T* rule for freeze and lambda are also now changed to strip all (dynamic X) entries from the hypothesis list like so:

(defprolog system-S-h

  (- [freeze Y]) [lazy B] Hyp  <-- (bind Hyp2 (filter-dynamic Hyp)) (system-S-h Y B Hyp2);)

***********

Problem 3. Extend the types for freeze/lambda

***********

Any usage of 'fluid-value' inside an expression requires there to be an active (dynamic (env | A)) in the assumption list.

Therefore the default version of freeze/lambda in T* should fail (because all (dynamic A) entries are stripped from the list).

So we need to add a new version that creates an empty dynamic context and tags the result type with it, as well as a new version of thaw (called 'inject' below):

(datatype freeze2

                            (dynamic (env | New)) >> X : A;
               _______________________________________________
              (dynamic (env | _)) >> \\ TODO: needs to strip all dynamic

                 (freeze X) : (context New (lazy A));

                            (dynamic (env | New)) >> X : A;
               _______________________________________________
                     (freeze X) : (context New (lazy A));

                         X : (context Want (lazy A));
                            (check-all Want Have);
                  __________________________________________
                       (dynamic (env | Have)) >> (inject X) : A;)

***********

Problem 4. Type fluid-let

***********

Note that it has to reach into the outer 'freeze' inside the body (if it exists) to inject the context below it, because the implementation of fluid-let needs to use lazy evaluation.

(datatype fluid-let

                         (update Key r A Have Have*);

                     (dynamic (env | Have*)) >> Body : C;
                _____________________________________________
                  (- (let-body Have Key A C (freeze Body)));

                                      !;
                          (dynamic (env | Have)) >> Value : A;
                        (let-body Have Key A C Body);
    ______________________________________________________________________
               (dynamic (env | Have)) >> (fluid-let Key Value Body) : C;

                                  Value : A;
                         (let-body () Key A C Body);
    ______________________________________________________________________
                       (fluid-let Key Value Body) : C;

                           (env? Key r A Have);
      _________________________________________________________________

                    (dynamic (env | Have)) >> (fluid-value Key) : A;)

***********

Notes

***********

You could avoid the modifications in 'problem 1' if you were to wrap the body of function 'test4' in a 'freeze', and thereby obtain the (context A B) type as a result, but it isn't really that great of an option.

The modifications in problem 1 are useful for other things anyway.

***********

Tests

***********

\\ these all work (the 'let!' macro just expands out fluid-let and fluid-value as needed):

(define test3
  { (context (*test2* : r number) (lazy number)) --> number }

  Thunk -> (let!

           *test* 1
           *test2* (+ 1 *test*)

         (inject Thunk)) )

(define test4
  { context (*test2* : r number) (number --> number) }

  N -> (+ N (fluid-value *test2*)) )

(fluid-let *test2* 10
           (freeze (test4 1)))

(let X (type (freeze (fluid-value *test2*))
             (context (*test2* : r number) (lazy number)))

   (fluid-let *test2* 0
              (freeze (test3 X))))

 

\\ And this one fails as intended

(let X (type (freeze (fluid-value *test2*))
             (context (*test2* : r string) (lazy string)))

   (fluid-let *test2* 0
              (freeze (test3 X))))

[nha...@gmail.com]

Updated the code to reflect the last post:

t-star2.shen: https://github.com/NHALX/shen-misc/commit/29a35e98481e67110364b2124a625d33c1463c82
env.shen: https://github.com/NHALX/shen-misc/blob/b6e884bef7f74de2630285d2edc331084194d862/env.shen

misc.shen: https://github.com/NHALX/shen-misc/blob/2b49a6204aa8638b7988529ac5a0b2fe66eb46df/misc.shen

[Mark Tarver]

Problem 1. T* only accepts basic type signatures.

OK.

(define test4
{ context (*test2* : r number) (number --> number) }
N -> (+ N (fluid-value *test2*)) )
 

Yes; T* won't take this but ...

(datatype ctx
                  (dynamic (env | P)), F : Sig >> (shen.intro F Rules) : A;
    ___________________________________________________________________________
                 F : (context P Sig) >> (shen.intro F Rules) : A;


      ______________________________________________________________________
              (dynamic (env | P)), F : (context P (A --> B)) >> F : (A --> B);


                                Rules : (A --> B);
                  ______________________________________________
                    F : (A --> B) >> (shen.intro F Rules) : C; )
                   

doesn't give any way of proving 'context' types; there is no right rule.  You cannot prove anything about test4.

M.

[nha...@gmail.com]

You just have to obtain a (number --> number) from (context (*test2* : r number) (number --> number)) and go about T* as normal.

test4 means "if you give me a (context (*test2* : r number) (number --> number)), and a number I'll return you another number"

All the proof obligations wrt pattern matching in the head is handled the same as before.

[nha...@gmail.com]

Here is the spy 'proof'

(62+) (define test4

  { context (*test2* : r number) (number --> number) }

  N -> (+ N (fluid-value *test2*)) )

____________________________________________________________ 3 inferences
?- test4 : Var2

>

typechecking (fn test4)
____________________________________________________________ 16 inferences
?- (shen.intro test4 (shen.rules test4 (shen.rule (N) (+ N (fluid-value *test2*))))) : Var10

1. test4 : (context (*test2* : r number) (number --> number))

>

____________________________________________________________ 37 inferences

?- (shen.intro test4 (shen.rules test4 (shen.rule (N) (+ N (fluid-value *test2*))))) : Var10

1. (dynamic (env *test2* : r number))
2. test4 : (number --> number)

>

____________________________________________________________ 70 inferences
?- (shen.rules test4 (shen.rule (N) (+ N (fluid-value *test2*)))) : (number --> number) \\ entering T*-rules prolog here

1. (dynamic (env *test2* : r number))

>

____________________________________________________________ 81 inferences
?- &&N : number

1. &&N : Var24
2. (dynamic (env *test2* : r number))

>

____________________________________________________________ 88 inferences
?- ((+ &&N) (fluid-value *test2*)) : number

1. &&N : number
2. (dynamic (env *test2* : r number))

>

____________________________________________________________ 96 inferences
?- (+ &&N) : (Var26 --> number)

1. &&N : number
2. (dynamic (env *test2* : r number))

>

____________________________________________________________ 104 inferences
?- + : (Var27 --> (Var26 --> number))

1. + : (number --> (number --> number))
2. &&N : number
3. (dynamic (env *test2* : r number))

>

____________________________________________________________ 108 inferences
?- &&N : number

1. &&N : number
2. (dynamic (env *test2* : r number))

>

____________________________________________________________ 113 inferences
?- (fluid-value *test2*) : number

1. &&N : number
2. (dynamic (env *test2* : r number))

>

____________________________________________________________ 122 inferences
?- fluid-value : (Var29 --> number)

1. &&N : number
2. (dynamic (env *test2* : r number))

>

____________________________________________________________ 197 inferences
?- (env? *test2* r number (*test2* : r number))

1. &&N : number

>

____________________________________________________________ 223 inferences
?- (unify (just number) (just number))

1. &&N : number

>

(fn test4) : (context (*test2* : r number) (number --> number))

[Mark Tarver]

     
doesn't give any way of proving 'context' types; there is no right rule.  You cannot prove anything about test4.

 I expect the answer to my question is that you've procedurally encoded the context rule into the Shen kernel.

OK some more questions.

1.   Does the notation (context Delta A) means 'Prove A in the context Delta'?

2.   Is F : (context (P | Ps) (A --> B)) significantly different from F : ((context (P | Ps) A) --> B)? If not, can you give an example?

3.   What is the shortest and simplest example you can provide where you prove the utility of context types?  Simple preferably means

      not assuming any machinery other than what already exists in Shen.

4.   Are context types a genuine extension of the expressive power of Shen or are they syntactic sugar for something that can be

      coded in Shen sequent calculus?  Can you show your answer to be true?

5.   How do you propose to change the applications rule which requires a function space type?   This can be done IMO but needs

      some attention.

                    F : (A --> B);   <--- problem here
                    X : A;
                    ______________
                    (F X) : B; 

M.

[nha...@gmail.com]

Keep in mind the modifications described in "Problem 1" are general and don't depend on the 'context' type in any way. The context type, however, depends on the modifications.

It is possible for the user to define other types which can be converted to (A --> B), which have whatever semantics they want. The main point here is to allow the caller to verify some arbitrary precondition at the call-site, using the contextual information available to it, and for this precondition to be transmitted indirectly to the callee via assumptions (injected by the type signature). The assumptions are valid, when type checking the function body, because there is no way to enter the scope of the callee without the preconditions being proven by the caller.

 'context' was a poor choice of name for the type because I've been using the word context to refer to different things in my explanations (there's a T* context referring to the hypothesis list, the context type itself which describes a dynamic binding environment, and the basic English usage of the word, all being used interchangeably which is making things ambiguous). 

 
1.) Sort of - it's possible to do that, but it is less general in the case of the 'context' type though because it is looking specifically for a (dynamic (env | A)) entry in the T* hypothesis list at the call site. The 'context type' here is basically just wrapping lambda, freeze and global function type signatures allowing them to have some constraints placed on their usage. It's not so different than verified types except the verification has to be done at the call site rather than inside the callee, which is important because the caller has more information  available about the local state of things.

2.) Yes I don't think the second type can be constructed. 'context' only wraps (A --> B) or (lazy B). Either way, the first F would be a first order function from A -> B, and the second F would be a higher order function which takes a lambda and returns a 'B'.

3.) I have to think of something simple that doesn't use any modifications, but again the modifications described here aren't dependent on the 'context' type or its definition in any way.

An example (which uses the T* modifications): 'test4' cannot be called without *test2* being dynamically bound to the correct type:

(fluid-let *test2* 10
           (freeze (test4 1)))

(define test4
  { context (*test2* : r number) (number --> number) }
  N -> (+ N (fluid-value *test2*)) )

4.) The modifications to T* (unrelated to the 'context' type) add more information into the type checking environment of a function body than was previously possible. A function can not be called, and a type cannot be constructed without the caller type checking it. Therefore if a datatype or function has side conditions wrt its construction, then you are free to add these side conditions as assumptions when type checking inside the body of function who's type signature mentions said types, because the function could never have been entered and the parameters cannot exist if the side conditions were not previously met at the call site. The proof is in the modified t*-rules function, which previously had an empty hypothesis list, but which now includes hypotheses generated by sequent calculus rules which unpacks assumptions that can be assumed from the declared type signature.       

5.) The definition of lookupsig is changed. Instead of unifying the signature directly it adds a level of indirection. 'F : Sig' is added to the hypothesis list and then it tries to prove F : (A --> B) from that. So if you have rules to generate a function type from another type (such as a constrained type like 'context' -- which can situationally generate the required (A --> B) if the local environment permits it) then it can proceed as usual.  

(defprolog lookupsig
  X A Hyp <-- (sigf (assoc (0 X) (value *sigf*)) Sig)

              (system-S-h X A [[X : Sig]|Hyp]);) 

As far as the context type is concerned, rules for lambda and freeze look like so:

(defprolog reset-dynamic#type
    (- [reset-dynamic Y X A]) Hyp <-- (bind Hyp* (append Y (shen.filter-dynamic Hyp)))
                                      (shen.system-S-h X A Hyp*);)

(shen.remember-datatype reset-dynamic#type (fn reset-dynamic#type))

(datatype @env-freeze@

           (reset-dynamic ((Y : A) (dynamic (env | New))) X B);
    ___________________________________________________________________
                  (lambda Y X) : (context New (A --> B));


               (reset-dynamic ((dynamic (env | New))) X A);
    ___________________________________________________________________

                   (freeze X) : (context New (lazy A));


                   X : (context Want (lazy A));
                      (check-all Want Have);

          _______________________________________________
            (dynamic (env | Have)) >> (inject X) : A;) \\ AKA thaw

6.)" I expect the answer to my question is that you've procedurally encoded the context rule into the Shen kernel."

Sorry, yes system-S-h has this as another clause:

  (- [rules F | Rules]) A Hyp     <-- (t*-rules F Rules A 1 Hyp);

and the top level T* which handles [define|...] generates the [intro|...] expression ('intro' is confusingly handled by sequent calculus rules instead of system-S-h):

 (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))
                            (is Intro  [intro F [rules F | FreshRules]])
                            (system-S-h Intro RealSig [[F : FreshSig]])
                            (is Sig A);)

And some plumbing is changed wrt to the hypothesis list.

The above is just a minimum low-effort way to achieve what was needed, there are better ways to organise it.

[Mark Tarver]

2.) Yes I don't think the second type can be constructed. 'context' only wraps (A --> B) or (lazy B). Either way, the first F would be a first order function from A -> B, and the second F would be a higher order function which takes a lambda and returns a 'B'. 

That's kind of a fiat. 

 5.) The definition of lookupsig is changed. Instead of unifying the signature directly it adds a level of indirection. 'F : Sig' is added to the hypothesis list and then it tries to prove F : (A --> B) from that. So if you have rules to generate a function type from another type (such as a constrained type like 'context' -- which can situationally generate the required (A --> B) if the local environment permits it) then it can proceed as usual.  

  I think 5. is going to be harder than that.  You cannot invoke the type of the function unless your contextual

 conditions are met and these will be lost back in the search because chances are they will relate to the

arguments to the function which have been processed.   

                    F : (context Ps (A --> B));   

                    Ps; <--- how to handle these?

                    X : A;
                    ______________
                    (F X) : B;

It is simpler to place the constraints in the type of F.

M.

--
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/c7ad28ff-8741-4bec-93d3-6e5e277a6667n%40googlegroups.com.

[nha...@gmail.com]

"That's kind of a fiat. "

Yeah, it's only that way because there are no rules to define the 'context' type that don't involve a lambda or function. The original problem was how to dynamically inject a binding environment while evaluating a thunk.

"because chances are they will relate to the arguments to the function which have been processed"

In this particular situation the preconditions aren't related to the function parameters, because it is a global (ideally thread local) state.

If you were to do F : (A --> (context Ps B)) as the alternative, you would have to wrap the function body in a 'freeze', which pushes the 'context' into the return type, but also changes the runtime behaviour of the function.

Wrapping the parameter types with constraints may be potentially more cumbersome overall.

In reply to the sequent you posted:

"""

                   F : (context Ps (A --> B));   

                    Ps; <--- how to handle these?

                    X : A;
                    ______________
                    (F X) : B;

"""

That's not how the new rule is setup for application though. The rule still says F : (A --> B) during application. 

You have to conjure up the F : (A --> B) from elsewhere to satisfy it. Like so:

                            (whatever P);

___________________________________________

   F : (context P (A --> B)) >> F : (A --> B);

Further to your second point:

Shen defines the order of evaluation for function parameters, so why not just push all the temporary parameter values into the hypothesis list with unique generated temporary names. This allows L-rules to interact with them while resolving the function application.

Alternatively convert all function applications to Administrative Normal Form while type checking (it is already modified by currying anyway)?

This may dramatically aid in debugging with spy (I often find myself splitting and let-binding some complex expressions that I have trouble debugging). 

Or maybe it is really annoying, I'm not sure, but regardless it doesn't have to be visible to spy if you do it a different way.

The code that currently curries the input expression already modifies function applications. 

(f a b) is currently changed to ((f a) b), but instead it could generate:

(let F' f

       A' a

       B' b

  ((F' A') B'))

This pushes all the temporary values onto the hypothesis list.

None of this is necessary to typecheck the original problem though. 

[Mark Tarver]

I think you need precise sequent rules for the context type; at the moment it seems a bit ungrounded.

I don't think anybody can precisely analyse these suggestions w.o. some more formal structure.

<< The code that currently curries the input expression already modifies function applications. 

(f a b) is currently changed to ((f a) b), but instead it could generate:

(let F' f

       A' a

       B' b

  ((F' A') B'))

This pushes all the temporary values onto the hypothesis list.  None of this is necessary to typecheck the original problem though. >>

Yes, but unless you can check applications the function is not usable. Doable solution; but a bit heavy going. 

<<

(whatever P);

___________________________________________

   F : (context P (A --> B)) >> F : (A --> B);                                   >>

You probably want

F : (context P (A --> B);

(whatever P);

_______________

F : (A --> B);

The whatever bit is in need of clarification.  

Also I suppose I don't see why this rule cannot be generalised to:

F : (context P A);

(whatever P);

_______________

F : A);

The other bit I wanted was a motivating example without fluid-lets etc.  

M.

[nha...@gmail.com]

"""Also I suppose I don't see why this rule cannot be generalised to:

F : (context P A);

(whatever P);

_______________

F : A);"""

Probably it can, but the original 'context' type wasn't for all context related things and just for the fluid-let problem, another reason why it was badly named.

"I think you need precise sequent rules for the context type; at the moment it seems a bit ungrounded. I don't think anybody can precisely analyse these suggestions w.o. some more formal structure."

It's all in the files I linked, but anyway let's try it with a simpler type.

'want' below must be called lexically within a 'block'.

(datatype prop
                    P, F : Sig >> (shen.intro F Rules) : TODO;
    ___________________________________________________________________________
                 F : (prop P Sig) >> (shen.intro F Rules) : TODO;
                                         
                                  F : B >> F : A;
      ______________________________________________________________________
                            P, F : (prop P B) >> F : A;


                                something >> X : A;
                          ______________________________
                                  (block X) : A;  )

(define block
  X -> X)

(define want
  { prop something (A --> (B --> number)) }
  X Y -> 1)

(block (want 1 "a")) \\ typechecks

(want 1 "a") \\ fails because 'something' missing

Here is the spy for type checking 'want':

typechecking (fn want)
____________________________________________________________ 16 inferences
?- (shen.intro want (shen.rules want (shen.rule (X Y) 1))) : Var10

1. want : (prop something (&&&A --> (&&&B --> number)))

>

____________________________________________________________ 61 inferences
?- (shen.intro want (shen.rules want (shen.rule (X Y) 1))) : Var10

1. something
2. want : (&&&A --> (&&&B --> number))

>

____________________________________________________________ 92 inferences
?- (shen.rules want (shen.rule (X Y) 1)) : (&&&A --> (&&&B --> number))

1. something

>

____________________________________________________________ 104 inferences
?- &&X : &&&A

1. &&X : Var24
2. &&Y : Var28
3. something

>

____________________________________________________________ 109 inferences
?- &&Y : &&&B

1. &&X : &&&A
2. &&Y : Var28
3. something

>

____________________________________________________________ 117 inferences
?- 1 : number

1. &&X : &&&A
2. &&Y : &&&B
3. something

>

(fn want) : (prop something (A --> (B --> number)))

***************************************

Test A (reject)

***************************************

(212+) (want 1 "a")
____________________________________________________________ 7 inferences
?- ((want 1) "a") : Var2


>

____________________________________________________________ 12 inferences
?- (want 1) : (Var4 --> Var2)


>

____________________________________________________________ 17 inferences
?- want : (Var5 --> (Var4 --> Var2))

1. want : (prop something (Var7 --> (Var8 --> number)))

>

____________________________________________________________ 57 inferences
?- want : (Var5 --> (Var4 --> Var2))


> 

shen error in shen.unwind-types: shen error in shen.type-error: type error

***************************************

Test B (success)

***************************************

(211+) (block (want 1 "a"))
____________________________________________________________ 7 inferences
?- (block ((want 1) "a")) : Var2


>

____________________________________________________________ 13 inferences
?- block : (Var4 --> Var2)


>

____________________________________________________________ 77 inferences
?- ((want 1) "a") : Var2

1. something

>

____________________________________________________________ 83 inferences
?- (want 1) : (Var4 --> Var2)

1. something

>

____________________________________________________________ 89 inferences
?- want : (Var5 --> (Var4 --> Var2))

1. want : (prop something (Var7 --> (Var8 --> number)))
2. something

>

____________________________________________________________ 136 inferences
?- want : (Var5 --> (Var4 --> Var2))

1. want : (Var7 --> (Var8 --> number))

>

____________________________________________________________ 140 inferences
?- 1 : Var7

1. something

>

____________________________________________________________ 143 inferences
?- "a" : Var8

1. something

>

1 : number

[Mark Tarver]

OK; to begin to clarify.  Then are two approaches here, because what you are dealing with are
contextual constraints.  Your suggestion is to place the constraints P outside the type.  Like this

Neal: P -> (all x A(x) -> B(f(x))).

Mine is to put it inside the type

Mark: all x ((P & A(x)) -> B(f(x))).

Are they equivalent?  No.

You can derive your formulation from mine by first-order reasoning but not vice versa.  The question is which suits the purpose?

I think one argument in favour of the Mark formulation is that it requires less digging up of the road
since you have to change T* and even the structure of the code being checked to follow Neal.

Here is a formulation of Mark

(datatype constraint
   
   let P* (no-prolog (shen.curry P))
   X : A; P* : (A --> boolean); (sat X P*);
   ======================================
   X : (- (constraint P A));
   
   if (ground? X)
   if (eval [P X])
   ___________
   (- (sat X P));)
   
(define ground?
  [X | Y] -> (every? (fn ground?) [X | Y])
  X -> (not (shen.freshterm? X)))
 
(define no-prolog
  [lambda X Y] -> (subst (newv) X [lambda X Y])  where (shen.pvar? X)
  X -> X)

Now the above LR rule says that X has the type (constraint P A) just when X : A, P is a boolean constraint on objects of type A

(a lambda expression) and X satisfies P.  The P* stuff is just to massage P into a suitable form.

The satisfaction rule just allows us to prove the the satisfaction test is met by applying the lambda expression P to X when X is fully

instantiated.    It works.

(31+) (define f
              {(constraint (/. X (> X 1)) number) --> number}
               N -> (- N 1))
(fn f) : ((constraint (lambda X (> X 1)) number) --> number)

(32+) (f 0)
type error

(33+) (f 2)
1 : number

Mark

[nha...@gmail.com]

That's a cool type definition, but it seems to solve a slightly different problem than the original.

1.) It requires a function parameter to attach to. (the original problem is tracking an implicit global state that isn't referenced by value anywhere)

2.) It won't tell if you function f was called while nested inside another expression (g f)

2.) The T* integrity check seems to breaks things if the function head pattern isn't a variable. 

3.) Also If the head pattern isn't a variable then you can't retain the (constraint P ...) information.

[Mark Tarver]

On Tuesday, 24 January 2023 at 22:55:38 UTC nha...@gmail.com wrote:

That's a cool type definition, but it seems to solve a slightly different problem than the original.

1.) It requires a function parameter to attach to. (the original problem is tracking an implicit global state that isn't referenced by value anywhere)

2.) It won't tell if you function f was called while nested inside another expression (g f)

3.) The T* integrity check seems to breaks things if the function head pattern isn't a variable. 

4.) Also If the head pattern isn't a variable then you can't retain the (constraint P ...) information.

1.     Put a dummy parameter into your 0-place function.

3.-4.     You need an extra rule to sat which says effectively to skip the sat test if the input is not ground.

(datatype constraint
   
   let P* (no-prolog (shen.curry P))
   X : A; P* : (A --> boolean); (sat X P*);
   ======================================
   X : (- (constraint P A));
   
   if (ground? X)
   if (eval [P X])
   ___________
   (- (sat X P));
   

   if (not (ground? X))
   ____________________

   (- (sat X P));)   

2.  When dealing with functions whose arity > 2 use a tuple to parcel up the inputs.

(35+) (datatype constraint

   let P* (no-prolog (shen.curry P))
   X : A; P* : (A --> boolean); (sat X P*);
   ======================================
   X : (- (constraint P A));

   if (ground? X)
   if (eval [P X])
   ___________
   (- (sat X P));

   if (not (ground? X))
   ____________________

   (- (sat X P));)

constraint#type : symbol

(36+) (define h
  {(constraint (/. X (> (fst X) (snd X))) (number * number)) --> (list number)}
   (@p M N) -> [M N])
(fn h) : ((constraint (lambda X (> (fst X) (snd X))) (number * number)) --> (list number))

(37+)  (h (@p 1 2))
type error

(38+)  (h (@p 2 1))
[2 1] : (list number)

Mark

[nha...@gmail.com]

"1.     Put a dummy parameter into your 0-place function."

The point of fluid-let is to avoid having to thread a state parameter through everything, so putting an extra parameter to satisfy the type checker is counter productive here.

"2.  When dealing with functions whose arity > 2 use a tuple to parcel up the inputs."

This still won't help you with (fluid-let *var* value (freeze (fluid-value *var*))) because there can be arbitrary nesting of expressions between the 'let' and 'value' expressions. 

[Mark Tarver]

Probably reached the end of my useful contribution.

If you want zero-place functions with constraint types then just say in the signature that the output has such-and-such a constraint type.  Effectively

a pure zero-place function is just a constant so it will be type checked as

a ground case and presumably passed.

I don't know about fluid-let but nesting functions which have constraint types is no problem.  The type checker will ensure that if f1 passes a result with a constraint type

to f2 which expects to receive a constraint type that the two constraint types 'match'.

The simplest match is if the constraints are identical but you can experiment with formalising additions to this.  

M.

--
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/Ufubur2qOFE/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/a7f428f9-5228-4a47-8eeb-e14503c382d2n%40googlegroups.com.

[nha...@gmail.com]

Hmm maybe this fluid-let stuff is better implemented with modal logic?

The concept of different variable binding scopes in fluid-let would seem to map nicely onto the concept of world states in modal logic.