Dependent types in function definitions

[nha...@gmail.com]

Is there any good way to do the below, without having to define 'with-file' as untyped in a different file and exporting a type theory for it. The following (right rule) works, but I would like the body of 'with-file' to be type checked as well. 

(datatype with-file
                        if (element? M [in out])
                             File : string;
                        K : ((stream M) --> B);  ________________________________________________________________
                       (with-file File M K) : B;)

Maybe it would be a good idea if the Shen loader was modified for typed files. Currently, if a type signature is missing from a function definition it will throw an error, but instead maybe it should query the type system to see if it was defined through sequent rules, and use the left rule for it to introduce the variables?

    File : string, M : M, K : ((stream M) --> B) >> P;

__________________________________________________________

              (with-file File M K) : B >> P;

(define with-file
\\  { string --> M --> ((stream M) --> B) --> B }
  Filename Mode K -> (let File (open Filename Mode)
                        (trap-error (let Result (K File)
                                       (do (close File)
                                           Result))

                                    (io-error Filename File))))

[nha...@gmail.com]

I guess maybe you need '(element? M [in out]) : verified' as well in the left rule.

[Mark Tarver]

There's nothing to stop you using dependent types in your derivation

rules; it's just that you cannot in Shen prove a function has a dependent type

- at least not beyond a certain point discussed in TBoS.  

A long time ago, in the time of SEQUEL, the system did indeed allow for 

implicit typing and if a function did not have a type SEQUEL would try to

infer it like ML.  The problem was that this was computationally very expensive

and people could be confused by the computer hanging so I made the decision 

to insist on explicit typing.

There is a very old thread on this.

https://groups.google.com/g/qilang/c/lppk3fyDG3U/m/10N5t24QhTsJ

Mark  

--
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/0c84a5b9-5417-4516-9637-28503fea7689n%40googlegroups.com.

[nha...@gmail.com]

It would still be explicit typing, just that the system pulls the type from a different location (the global database, vs the local type signature).

Say you have:

(define f X -> (+ 1 X))

It then queries the global database for:

(f X) : A

where there's a user defined rule saying

   X : number >> P;

_________________________

  (f X) : number >> P;

which the type checker can use to introduce X when proving the body of the function.

This way you have full access to all the features of Shen's type system when defining a function's type signature.

You could even have a function have multiple types this way and prove that each signature still leads to a correct function body. 

[nha...@gmail.com]

The top level of the function is proving: (f X) : A >> (+ 1 X) : A

[Mark Tarver]

You certainly can do experiments in that direction; https://shenlanguage.org/TBoS/tbos_278.html#34; would be a place to start.    The derived types could be asserted as sequent rules which you would need for functions that are ad hoc overloaded wrt types.    At some point you might leave T* behind though.    T* builds its speed on making hard-wired decisions about the nature of the proof process.

Mark

[Mark Tarver]

This might give some ideas.

(datatype with-file

    let Disable (enable-type-theory -)    \\ a clean slate
    let Enable (include Theories)             \\ try with your ideas
    Theories : (list symbol);
    File : string;
    (disable Theories);
    ________________________________
    (with-file File Theories) : symbol;  \\ see def of with-theory
   
    let Enable (enable-type-theory +)        \\ if rule 1 fails, restore settings
    let Disable (preclude Theories)    
    if false                                                       \\ make sure this fails
    ________________________________
    (with-file File Theories) : symbol;
   
    let Enable (enable-type-theory +)        \\ if rule 1 succeeds. restore settings
    let Disable (preclude Theories)

    Theories : (list symbol)
    __________________________
    (disable Theories);)
   
(define with-file
  File _ -> (let Code (read-file File)
                        Eval (map (fn eval) Code)
                        loaded))

Mark

[Mark Tarver]

actually one correction

\\ see def of with-file

I thought with-theory or with-theories might be a better naming.

Mark

[Mark Tarver]

  Actually you need to load the actual code

  let Disable (enable-type-theory -)  \\ a clean slate
    let Enable (include Theories)       \\ try with your ideas

    let Code (read-code File)

    Theories : (list symbol);
    File : string;

    Code : <put your type here>;        \\ decide what you want to do here
    (disable Theories);
    ________________________________
    (with-theory Code Theories) : symbol;  \\ see def of with-files

How you load the code is up to you.  One possible way is as a tuple.

(define read-code

     File -> (form-tuple (read-file File)))

(define form-tuple

    [] -> eof

    [X | Y] -> (@p X (form-tuple Y)))

So the type of the code in the file is a tuple of the types in it according to your theories.

M.

[Mark Tarver]

Actually you are building the representation of a tuple and not a tuple

(define form-tuple

    [] -> eof

    [X | Y] -> [@p X (form-tuple Y)])

Right that's an end to virtual hacking into email.   I'll leave the developments in your hands.

bw

M.

[nha...@gmail.com]

Regarding the performance implications on the type checker: instead of having no type signature result in the global lookup, you could instead specify a specific named 'datatype' rule to consult, instead of having it run through the whole type database.

Something like:

(define f

  { somerule#type }

  X -> X)

This doesn't seem like a major restriction, and you are cutting down the search space to probably only a single top level choice point in most cases.   

[Mark Tarver]

Well you could - but you might as well just state what it is you expect to prove if you're 

so sure that you know exactly what is needed to prove it.

M.