Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision Last revision Both sides next revision | ||
|
a_type_system_as_a_model_for_some_concepts [2016/09/21 16:52] nikolaj created |
a_type_system_as_a_model_for_some_concepts [2016/10/16 14:51] nikolaj |
||
|---|---|---|---|
| Line 2: | Line 2: | ||
| | [[Drawing arrows and coding functions]] $\blacktriangleright$ A type system as a model for some concepts $\blacktriangleright$ [[Foundational temp1 ]] | | | [[Drawing arrows and coding functions]] $\blacktriangleright$ A type system as a model for some concepts $\blacktriangleright$ [[Foundational temp1 ]] | | ||
| ==== Guide ==== | ==== Guide ==== | ||
| - | (We introduce some basic notions of Idris and discuss it in terms of some category theoretical notions, as discussed in | + | We introduce some basic notions of Idris, namely those that can be seen as "semantics" for logic, set theory and category theory (or rather topoi, as discussed in |
| - | [[http://arxiv.org/abs/1212.6543 | Leinster, Rethinking set theory]]. | + | [[http://arxiv.org/abs/1212.6543 | Leinster, Rethinking set theory]]). However, we always treat the (chosen subpart of the) language from a syntactical perspective as a programming language, //as is//, and don't "force it into" a known mathematical structure. (In particular, many forms of "equality" often make problems.) |
| - | The code presented below is also all included on the page [[Idris syntax]].) | + | |
| + | (161013 The code presented below is also all included on the page [[Idris syntax]], but that's just for now.) | ||
| === tmp Overview === | === tmp Overview === | ||
