I am learning logic and functional programming and there is a topic called Type checking and their relationship to logic , I am unable to find any source that can help me in understanding this topic. Please help .
https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ - This book.
A type for a parameter is like a precondition, and a type for a return value is like a postcondition. Structs function as an AND operator, and Unions function as an OR operator. When you say
performTransaction(x : DollarAmount) : Result
If x had to be constructed as a valid DollarAmount type, then this function is only callable if that was possible. Also, the Result type is guaranteed to have some fields on it (error codes, transaction id, etc); and performTransaction has to construct the object to give it to you. So, if you view statements like "x : int" as "x is proven to be an integer", then it is not a stretch to have something more elaborate like: " x : int, x > 0, x < MAXINTEGER " to assert that x is a positive integer (a DependentType is a type that depends on the value, typically notNull, notZero, etc).
You can make functions take in very specific types that indicate an initial state, and return new types that indicate new states; and use types to enforce constraints on following a state machine - at compile time in many cases.