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