type-check auto doesn't check in add-atom

[AdrickTench]

Setting type-check to auto doesn't catch type errors in add-atom. This seems undesirable. As far as I know add-atom &self A is the same as just A, so why should add-atom get to bypass type-checking if it has been enabled.

!(pragma! type-check auto)
; (= (foo $x) (+ $x "2")) ;; this errors
!(add-atom &self (= (foo $x) (+ $x "2"))) ;; this should error but doesn't
!(foo 1) ;; this errors because the previous line successfully adds the bad definition for foo

[vsbogd]

Thanks for raising this question. add-atom passes type-check because of its type signature (-> hyperon::space::DynSpace Atom (->)) and Atom allows passing any atom without type-checking. This behavior doesn't contradict to the type checking algorithm we have but I agree it can cause the confusion.

The ability to add incorrect atoms into atomspace is implemented intentionally because when new information is added into atomspace in the future the types of atoms can be changed and type check can be passed. It is not clear to me should we prevent this when type-check auto is on even when atom is added manually. We could also go further and prevent using incorrect atoms in a program during static type-check even when function has an argument with meta-type Atom or Expression. Anyway it is clear that runtime check should allow passing incorrect atoms as an argument in such case. To me it sounds reasonable enough but I would also listen to @Necr0x0Der and other opinions.

On the other hand if one generates code automatically and want it to be type-checked before adding generated code into atomspace then there is a lack of instruments to do this. We could solve it by adding a function to do a type-check in a runtime manually. Using such function one will be able to check generated code for a type correctness before adding it into the atomspace if it is needed.

@AdrickTench could you please elaborate whether you have some specific goal in mind when writing the code above or what bothers you is a discrepancy between implicit and explicit adding atoms into atomspace?

[vsbogd]

if one generates code automatically and want it to be type-checked before adding generated code into atomspace then there is a lack of instruments to do this.

@Necr0x0Der , suggested using !(get-type (= (foo $x) (+ $x "2"))) as a type check function. If it returns Empty then atom has an incorrect type. So actually we have such instrument already.

[vsbogd]

We could also go further and prevent using incorrect atoms in a program during static type-check even when function has an argument with meta-type Atom or Expression.

Discussed it with @Necr0x0Der offline. He suggested adding more strict variant of the type-check pragma (for example type-check auto-strict). While it is possible doing this but I am not sure whether this has a high priority or needed at all.

[AdrickTench]

could you please elaborate whether you have some specific goal in mind when writing the code above or what bothers you is a discrepancy between implicit and explicit adding atoms into atomspace?

Yes, the discrepancy between implicit and explicit bothers me. I was also trying to write tests for behavior with !(pragma! type-check auto). The constructs assertEqualToResult and assertEqual evaluate the form, so it's not clear how to write test cases for the behavior of implicitly adding atoms to the space. I was hoping to use add-atom to write test cases that verify the type errors generated when type-check is set to auto.

@TeamSPoon suggested I might instead write tests for type errors are generated by type-check auto by loading files, but I haven't been able to get that to work in hyperon. I tried these calls:

> !(import! &self "/home/atench/mettalog/development/metta-testsuite/test-scripts/type_check_auto_forms.metta")
[(Error (import! GroundingSpace-top "/home/atench/mettalog/development/metta-testsuite/test-scripts/type_check_auto_forms.metta") import! expects a module name as the first argument)]
> !(include "/home/atench/mettalog/development/metta-testsuite/test-scripts/type_check_auto_forms.metta")
[(Error (include "/home/atench/mettalog/development/metta-testsuite/test-scripts/type_check_auto_forms.metta") include expects a module name argument)]

[TeamSPoon]

re-pinging @vsbogd since he'd know for sure the syntax for loading files in H-E that would use the type checker.

some thoughts though:

The !(pragma! type-check auto) might need to be in the file containing (= (foo $x) (+ $x "2")) and not the file loading the file.

and loaded into a new space like: !(import! &my-other-self "local_file~need_typecheck") with the real file will be in the same directory on disk as local_file~need_typecheck.metta. ( The tilda is there since the testsuite has a hack to not treat files with it as toplevel test files.)

Personally I think much hard coded type checking wont be savvy enough to catch non obvious type errors sometimes.

If anything, it should only issue a warning and not errors (for instance then it could be safe to let add-atom warn about these things).

Also any type check tool will probably want be called by a developer when they think everyhting is loaded and ready for type check (or LSP server) to able do type check their convenance like (type-check &my-space) and get the list of warnings

[vsbogd]

I was also trying to write tests for behavior with !(pragma! type-check auto)

Am I right that you faced the issue when you was trying to write a test for !(pragma! type-check auto)? If what is needed is implementing tests for a type-checker then using get-type is a more convenient way. !(get-type <atom> <space>) returns Empty when type-check fails and vice versa. They use the same call of the type-checker.

[vsbogd]

The !(pragma! type-check auto) might need to be in the file containing (= (foo $x) (+ $x "2")) and not the file loading the file.

Yes, it is true. !(pragma! type-check auto) should be used in the module which needs to be type-checked and it doesn't affect child modules.

Personally I think much hard coded type checking wont be savvy enough to catch non obvious type errors sometimes.

Yeah, it is the reason why type-check auto is a pragma and it is off by default.

If anything, it should only issue a warning and not errors (for instance then it could be safe to let add-atom warn about these things).

It is nice idea. At least we could add another type-check state to show warnings instead of errors. One issue with making this default behaviour is that it can slow down execution because at the moment type-check is expensive.

Also any type check tool will probably want be called by a developer when they think everyhting is loaded and ready for type check (or LSP server) to able do type check their convenance like (type-check &my-space) and get the list of warnings

Yes it is possible using get-type and I can wrap it into another function lets say type-check to make it more recognizable.

[vsbogd]

type-check auto is an instrument for a developer to see type issues on a module loading time before execution. It is more a tool for a scripts development and it is not intended to use in a runtime. Usually runtime type-checks with type-check pragma turned off should be enough.

[AdrickTench]

OK, I can write tests of get-type as a rule. Still, it would be good to have at least a few tests cases that verify type-check auto specifically works as intended.