Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
a_type_system_as_a_model_for_some_concepts [2016/10/16 14:51] nikolaj |
a_type_system_as_a_model_for_some_concepts [2016/10/16 14:59] nikolaj |
||
|---|---|---|---|
| Line 3: | Line 3: | ||
| ==== Guide ==== | ==== Guide ==== | ||
| 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 | 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]]). 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.) | + | [[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. Then again, it's always good to know how to map your stuff //into// mathematical frameworks (e.g. into a well defined category), even if that mapping is neither surjective nor even injective. |
| (161013 The code presented below is also all included on the page [[Idris syntax]], but that's just for now.) | (161013 The code presented below is also all included on the page [[Idris syntax]], but that's just for now.) | ||
