# Math behind ocaml type system

**URL:** <https://discuss.ocaml.org/t/math-behind-ocaml-type-system/9982>\
**Category:** Community\
**Created:** [June 6, 2022, 10:43pm UTC](https://discuss.ocaml.org/t/math-behind-ocaml-type-system/9982 "2022-06-06T22:43:16Z")\
**Posts on this page:** 6\
**Page:** 1

<div class="post-metadata">

**Author:** ![devosalain](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/devosalain/32/3325_2.png) [@devosalain](https://discuss.ocaml.org/u/devosalain)\
**Post date:** [June 6, 2022, 10:43pm UTC](https://discuss.ocaml.org/t/math-behind-ocaml-type-system/9982/1 "2022-06-06T22:43:16Z")

</div>

Does there exists mathematics, theoretic behind ocaml type system.  
[PS : I learned recently lambda calculus is untyped]

---

<div class="post-metadata">

**Author:** ![yawaramin](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/yawaramin/32/3384_2.png) [@yawaramin](https://discuss.ocaml.org/u/yawaramin)\
**Post date:** [June 7, 2022, 1:12am UTC](https://discuss.ocaml.org/t/math-behind-ocaml-type-system/9982/2 "2022-06-07T01:12:52Z")

</div>

Refer to [Is there a informatic theory behind ocaml](https://discuss.ocaml.org/t/is-there-a-informatic-theory-behind-ocaml/9862)

---

<div class="post-metadata">

**Author:** ![shonfeder](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/shonfeder/32/424_2.png) [@shonfeder](https://discuss.ocaml.org/u/shonfeder)\
**Post date:** [June 7, 2022, 1:58am UTC](https://discuss.ocaml.org/t/math-behind-ocaml-type-system/9982/3 "2022-06-07T01:58:05Z")

</div>

There is indeed! For the root formal system, see [System F - Wikipedia](https://en.m.wikipedia.org/wiki/System_F)

---

<div class="post-metadata">

**Author:** ![EricGT](https://avatars.discourse-cdn.com/v4/letter/e/f1d935/32.png) [@EricGT](https://discuss.ocaml.org/u/EricGT)\
**Post date:** [June 7, 2022, 8:53am UTC](https://discuss.ocaml.org/t/math-behind-ocaml-type-system/9982/4 "2022-06-07T08:53:10Z")

</div>

> [@devosalain](#):
>
> Does there exists mathematics, theoretic behind OCaml type system.

While this site is definitely the place I would ask an OCaml question, since your question has another foot based in the world of type theory you might also ask at the StackExchange [Proof Assistants](https://proofassistants.stackexchange.com/) site for related information.

> [@devosalain](#):
>
> [PS : I learned recently lambda calculus is untyped]

Lambda Calculus started without a typing system. However the ancestry of Lambda Calculus is deep and varied. ([ref 1](https://proofassistants.stackexchange.com/a/940/5))

* * *

You might find this of interest: [Solving the halting problem](https://crypto.stanford.edu/~blynn/lambda/simply.html) (Don’t let the title fool you, this is about Lambda Calculus and explains why Lambda Calculus with types is useful).

---

<div class="post-metadata">

**Author:** ![EmileTrotignon](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/emiletrotignon/32/5913_2.png) [@EmileTrotignon](https://discuss.ocaml.org/u/EmileTrotignon)\
**Post date:** [June 7, 2022, 9:01am UTC](https://discuss.ocaml.org/t/math-behind-ocaml-type-system/9982/5 "2022-06-07T09:01:53Z")

</div>

I followed a course on type systems, that was taught by someone from the research team that works on ocaml, notes are available here : [http://cambium.inria.fr/~remy/mpri/cours.pdf](http://cambium.inria.fr/~remy/mpri/cours.pdf)

---

<div class="post-metadata">

**Author:** ![devosalain](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/devosalain/32/3325_2.png) [@devosalain](https://discuss.ocaml.org/u/devosalain)\
**Post date:** [June 7, 2022, 11:51am UTC](https://discuss.ocaml.org/t/math-behind-ocaml-type-system/9982/6 "2022-06-07T11:51:35Z")

</div>

The name F is coming back.  
Here a language F\* which is supposed to compile to F# and Ocaml,  
[https://www.fstar-lang.org/tutorial/](https://www.fstar-lang.org/tutorial/)