@plragde i think i read that clojure’s type system allows for defining types as predicates ???

very possibly miss remembering but i think clojures type stuff is based on the “specs” that are possible in clojure (and racket) however i very may well be getting totally confused ont hat!!! lol

@chris613 clojure’s specs are like Racket’s contracts

they aren’t types

ahhhhh maybe i missed something, i thought clojures “type” system was essentially an introspection of the specs to make sure they were compatable

@plragde I’m not sure what you’re suggesting. What is this technology?

@samth I think “the technology” in that sentence was just referring to the prior mention of systems like Coq and Agda (and dependently typed languages in general).

Which in turn was answering @isomorphisms’s question.

I might be blocked today but I just noticed something in the contract docs that I can’t find an example for. There’s this contract in the docs: (integer? string? ... integer? . -> . any) but I can’t find any function definition that satisfies the contract. The reason I am surprised is because I didn’t think having domain contracts after ... would work. A quick grep in racket code shows the use of ... in -> contracts is very rare and one with a domain contract after ... is non-existent except for the occurence in the documentation.

@pocmatos I don’t know what’s up with that specific doc example, but as background info: I think the support for ... in -> contracts was added sometime in the last couple of years, and it’s not well advertised in the docs. So a lot of code doesn’t use it. However, I use it all the time in my code and I wish ->* and ->i supported it too.

whoops just noticed I posted this in beginners. should be fine, i guess.

@notjack yes, i noticed it’s recent but still can’t find a function definition for a function satisfying the contract, do you know one?

My worry is of course, that if there are no tests and no code using this specific case, it might have gotten broken and nobody noticed.

I don’t know of any functions with a contract like that. I’m surprised the contract system even allows that at all.

there are a few things that use the “last argument” pattern seen there, although I don’t know if they are used with contracts anywhere

1. one of the functions passed to chaperone-procedure works like that

1. I think continuation prompt handlers work that way

I would recommend against doing that in your own APIs, it’s difficult to read and use

yes, I agree with that, I hate it

but what would be a function a definition satisfying such contract? (define (f n1 s1 s2 n2) ...) doesn’t satisfy and (define (f n1 . s n2) ...) is not valid. I am confused!

You’d declare the function (define (f i . args) ....) and split args by hand. Or use define/match or something.

woot? that’s ridiculous…

ahhhhhhh, now I understand. ok.

basically there’s no function definition syntax matching the contract syntax. But since the checking it’s done at runtime, it doesn’t matter. ugh, ugly.

thanks @lexi.lambda

Right. Racket’s define form can’t pull apart that particular argument list for you in the way you’d like, but ultimately, it’s still just a function that takes two or more arguments.

@pocmatos fyi, all of a contract’s checks on the “shape” of the arguments a function accepts are done at runtime. The contract has no way of knowing how you wrote the define clause for the function it’s attached to.

but the simpler cases usually just use procedure-arity and procedure-keywords

(so it’s a single check at the time the contract is attached to the function rather than a check every time the function is called)

right, i know. but my brain still tends to pattern match the contract using -> with the function definition.

which is probably a good thing to do and a habit that the contract APIs should encourage

i think i need to add an example to the docs so nobody is again made feel stupid by this particular syntax. :slightly_smiling_face:

I think that’s a wonderful idea

as an aside, I would really like it if ellipses were supported in define and #%app statements so I could write this: (define (my+ xs ...) (+ xs ...))

actually i wonder if it makes sense to put a code example in the reference guide (https://docs.racket-lang.org/reference/function-contracts.html) given there are no code examples there. It would make more sense in the guide but the guide doesn’t mention this syntax (probably on purpose)…

more examples everywhere are good

hi all

is anyone about that might be able to help me out with some datalog ??

sure!

really strugling to understand how to impliment a rule that says “X is in set A if X is part of set B but not part of set C”

I think the datalog language doesn’t provide negation

ahhhh

can i do it in the racket interop mode ??

(datalog family (? (add1 X :- 2))) <— dont understand this one :wink:

but i can see its using “normal” racket functions add1 ?

part of datalog’s design is to avoid negation so that it can provide various correctness and performance guarantees

no, it’s a fairly fundamental limitation of how datalog works

hmmmm

so is there annother way i should be thinking about the problem ?

I think so

What sort of rules are you making?

i want to be able to model statments & validations and then query for things that are unvalidated

(datalog blah (! (product)) (! (cost product 300)) (! (meets-need product "respond to rfis")) (! (average-salary sales 10000)) (! (statement "The target consumers are profesionals who's responsibilities include responding to RFI/RFP's.")) (! (responsibility sales "respond to rfis")) (! (responsibility presales "respond to rfis")) (! (statement sales "do not want to maintain a database")) (! (statement sales "are willing to work within a new environment (editor)")) (! (statement managers "get in the way")) (! (validation managers "get in the way")) (! (validation sales "do not want to maintain a database")) (! (:- (customer X) (responsibility X "respond to rfis"))) (! (:- (learning C X) (statement C X) (validation C X) (customer C))))

that could work if you model validations as rules that say “this thing is invalid when this condition holds”

but then I think you won’t be able to query for things that are valid (disclaimer: I am not a datalog expert and have barely used it)

hmmmm yeah i kinda wanted / need to ability to do both

you might be able to do it by writing rules for both

so would “upgrading” to racklog get me out of this problem ?

i tried messing about with rack log but the complexity killed me so i went back to datalog

I think you would be able to do this with racklog, yeah. I’m not sure whether it would be easier to use racklog or to use datalog in a restrained way (meaning, write both “isvalid” and “isinvalid” rules for each of your validation conditions)

i was just thinking about ” restrained way ”

would it be possible to write a third rul to ensure each statement has either one or the other valid / invalid

hmmmm

I don’t know but I suspect not.

hmmmm okies thanks a ton @notjack :slightly_smiling_face:

happy to help :simple_smile:

I just meant systems handling formal proof, such as Coq or Agda.