New answers tagged

0

The uncurrying process will lead to existential types. Since the adjoint of $(X\to)$ is $(X\times\vphantom{Y})$ and the adjoint of $(\forall X.)$ is $(\exists X.)$, it is appearently inevitable. Also, it will lead to types depending on terms (where simple types only depends on types themselves, and polymorphism allows terms to depend on types). So generally ...


-3

A "category" is just the compute graph. Functional Programming assembles a cat in the background but it's not obvious because you work thru monads. TensorFlow etc. makes assembly of the cat more obvious. Did Functional Programming Get It Wrong? by reinman


5

These colleagues of yours, would they happen to be Haskell aficionados? They might have told you that Hask was a category made from Haskell, but that is a lie, notheless a very useful one that inspires new programming techniques. If you would like to find out how category theory informs functional programming, I can recommend Bartosz Milewski's Category ...


2

A refinement type is a type together with a decidable predicate: $$ \{x:T ~|~ p(x)\} $$ where $x$ is a variable name, $T$ is a type, and $p(x)$ is a decidable predicate over $x$. A dependent pair type is the product type of two types where the second type depends on the value of the first: $$(x : T) \times q(x)$$ where $x$ is a variable name, $T$ is a type ...


Top 50 recent answers are included