Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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] (current)
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.)
Link to graph
Log In
Improvements of the human condition