Racket’s contract system is so cool!

it kind of works like type annotations in a language like Python, except instead of providing information for static analysis from an LSP, these are checked at runtime and they’re much more granular than just checking types

for example in Python I could write a simple Collatz function like this:

def collatz(max_: int) -> list[int]:
    ...

and that would tell my LSP that max_ is an integer and this function should return a list of integers. but in Racket I can do:

(define/contract (collatz max)
  (-> positive-integer? (listof positive-integer?))
  ;; ... code for the collatz function goes here
  )

and what this means is that max must be a positive integer, and collatz must always return a list of positive integers. if anything else happens, that will cause a contract error at runtime

so you’re not just defining what types your functions take - you’re also defining what specific kinds of values you’re expecting! and you can even define your own contracts from scratch, almost like writing your own assert statements (except it’s also kind of like defining a new type of data)

the one downside to this is that the Racket LSP can’t statically check contracts - they have to be checked at runtime. but still, it’s so cool

@kasdeya you might like LEAN4 :3 there you can be forced pass propositions (via dependant types) that some variable is sonething, by having a proof (its type is a proposition) of what the function you're calling wants :3

@zeichenreihe omgg I just looked up LEAN and it scares me lol. like it seems pretty cool - it seems like it’s able to solve equations at compile time and turn them into constant values? and maybe it can also mathematically prove that certain functions will always be correct, which sounds really cool if that’s a thing that it cna do

but this type of advanced math scares me lol - you can’t even google what something like ∀ means or what a lot of the jargon is

@kasdeya you'd have to provide proof yourself of correctness
and equation solving is limited but somewhat possible, but not for simplifying programs I think

basically you can have the following (in say python or java):

• a function f to create an object of type T
• a function g that requires an argument of type T
• nothing elsethen, to call g, you must provide a value of type Tin most cases, that could be a string or an integer (which you can create at any time by just typing it) but the object of type T only has one possible source: the function f.so having an object of type T means you were able to call f

this corresponds to mathematical proofs which also take things in (assumptions) and give you a proof of a statement.
that statement is encoded as a type T, so having an object of that type means having a proof of the statement.

the dependant in the dependant type theory it's based on is about that that T can contain other variables :3

for searching the funny maths symbols I recommend having a github search of the mathlib4 repo open and just /F/ (where F would be the symbol)
be prepared for very general definitions of things, as mathlib tries to formulate all of maths :3

oh and for more common maths symbols, look at the List of LaTeX mathematical symbols for getting a longer (more searchable) name and/or a short description :3 wikipedia also has redirects from some of the funny symbols to the "longer title" pages of them :3

@zeichenreihe ooh I think I see what you’re saying! so if f(n) validates that n is odd and then creates an OddNumber(n), then you know that every OddNumber is in fact odd. so the type itself tells you something about the value it contains. which means that f is a function that proves something about n and then returns n wrapped in that proof

that’s a little bit like how I’ve been using structs in Racket actually - for example in my simple tic-tac-toe game I have a (coords x y) struct which validates that x and y are non-negative integers between 0 and 2 inclusive. which means that I can have functions which take a coords and not have to worry about validating those things about the x and y values

and thank you for the tips about searching for math symbols! mathlib4 and LaTeX might be great resources - although I tend to find Wikipedia descriptions of math things very hard to make sense of lol

@kasdeya (not sure if its already clear, sorry if im repeating myself)
its like that but one level higher: the type Odd n (lean diosnt use any parenthesis for calling functions/types) doesnt even carry n as a value. the value of n is in the type, so Odd 1 and Odd 3 arent the same type :3
the values of these types are then 'the proofs' that tell you that 1 or 3 is odd, but these values arent relevant, since only the type carries all information :3
a function taking an number and the info that it is odd would then have arguments (n : Nat) (h : Odd n) where h stands for hypothesis (as in 'let n be an odd number'
:3

@zeichenreihe woahh - that is really hard to wrap my head around lol. I’m not sure if I understand at all in that case. but that’s okay! this type of stuff tends to be difficult for me anyway hehe