search

singnet / ai-dsl

Artificial Intelligence Domain Specific Language (AI-DSL) to enable autonomous interoperability between AI services.
MIT License
70 stars 18 forks source link

load the type definitions for different functions from external sources #7

Open kabirkbr opened 3 years ago

kabirkbr commented 3 years ago

I want to define service attributes and their metadata in external data structure (most probably json) and then provide an ability to load this metadata to idris type definitions for type checking and other magic, as specified with the following issues from NuNet worklfow:

I believe this is related to these places in the code: https://github.com/singnet/ai-dsl/blob/da959fe038e5c9c9955783d7418c59911859396c/experimental/RealizedAttributes.idr#L19 https://github.com/singnet/ai-dsl/blob/da959fe038e5c9c9955783d7418c59911859396c/experimental/ServiceAttributes.idr#L13 and similar.

Essentially what is required is to load the function / type definitions used in combine from external sources. is that possible at all and what is the best way to go about it? @ngeiswei @sroberti

ngeiswei commented 3 years ago

So, @kabirkbr , you're suggesting to translate the types and attributes stored the json structures used to describe snet services into idris and then use its type checker to very that they match, and that sounds good to me.

As for the code you mentioned in RealizedAttributes.idr and ServiceAttributes.idr, yes it would be it but note that it is experimental and incomplete at that point (ServiceAttributes.idr is a more elegant, albeit incomplete, alternative to RealizedFunction suggested by @sroberti, and RealizedFunction doesn't currently compile, though I'm gonna try to fix it today). The only stuff that is "complete" and compile (albeit limited and inelegant) is SimpleRealizedFunction (or equivalently, and probably better, SimpleDataRealizedFunction).

sroberti commented 3 years ago

I'll have to dig a bit deeper into the requirements here to see whether or not this is overkill, but Type Providers might be the best solution for converting external metadata into types usable for typechecking instead of loading them at runtime.

As far as this metadata goes, which properties are we most interested in verifying? Some things, like guaranteeing that a sequence of services does not exceed a cost threshold, are relatively simple, but it may be much harder to prove that some piece of self-reported JSON metadata accurately reflects the attributes of the service it represents. There might be some detail of the marketplace that I'm unaware of that'd make that a non-issue, though.

kabirkbr commented 3 years ago

@ngeiswei, yeah, this is the suggestion. the issue is that I am not sure what is the best way to do that and if there is an 'idris' style for that. the only thing that i can think of now is to do this through rather primitive string concatenations..

As far as this metadata goes, which properties are we most interested in verifying?

i suppose the only aspect that I can define and check in this situation are input and output types and i'd like to start only with them. however, i am not sure how to construct the type checking that would pass only on this level and i did not find the example in experiments. i think i will need some help here...

Some things, like guaranteeing that a sequence of services does not exceed a cost threshold, are relatively simple

hm, i think they may be simple on the idris side when all values are statically defined, but in real situations they may need to be instantiated dynamically during 'run time' which will involve extra-idris parts of the whole system -- and this is what I am thinking about. consider a situation when a service container is deployed on a random machine on a network which has its specific price for computational resources.

but it may be much harder to prove that some piece of self-reported JSON metadata accurately reflects the attributes of the service it represents

i am quite sure that this is not possible in formal sense (or at best not feasible to pursue at this point) -- irrespective of the external data format used. in the overall picture, we may need to resort here on the market mechanisms / reputation systems, statistical methods (i.e some sort of mechanism allowing to record success/failure of service calls within the network) , etc. that is yet another reason to build data structures accessible for processes external to idris...

There might be some detail of the marketplace that I'm unaware of that'd make that a non-issue, though.

there are many details, but i am not sure they make anything a non-issue, so thanks for the questions @sroberti -- these are exactly what i'd like to figure out..

ngeiswei commented 3 years ago

@kabirkbr said:

hm, i think they may be simple on the idris side when all values are statically defined, but in real situations they may need to be instantiated dynamically during 'run time' which will involve extra-idris parts of the whole system -- and this is what I am thinking about. consider a situation when a service container is deployed on a random machine on a network which has its specific price for computational resources.

Generally speaking the idea would be to replace fixed costs by a function that depends on the input. So for instance if the service is to reverse a list (to give an unrealistically simple example), the cost is gonna depends on the size of the list. For more complex tasks it may depends on the content of the list, etc, things can get quite complex. And then if it cannot be known deterministically (or is too hard/complex to calculate) then probabilistic abstractions can be used. In that case it could be a probability distribution (or second order probability distribution) over costs conditioned on inputs, etc.