id: a9d43327ead64ee1b67a1a6d07b99a40
parent_id: 8f46a08091c24502aa3e6493a20bbd21
item_type: 1
item_id: c66c0433c6a14de9b9a40e5a7316e382
item_updated_time: 1696250236902
title_diff: "[]"
body_diff: "[{\"diffs\":[[1,\"# Todo\\\n\\\n - [ ] wtf is a Horn clause\\\n - [ ] look up finite monomorphisation\\\n - [ ] overview of typedness (untyped, monomorphic, polymorphic, rank-n?, dependent)\\\n\\\n\"],[0,\"# Papers\"]],\"start1\":0,\"start2\":0,\"length1\":8,\"length2\":169},{\"diffs\":[[0,\"ofc.\"],[-1,\" TODO write an overview of those?\"],[0,\"\\\n\\\nDi\"]],\"start1\":6240,\"start2\":6240,\"length1\":41,\"length2\":8},{\"diffs\":[[0,\"s\\\"; \"],[-1,\"TODO wtf is a horn clause\"],[0,\"\\\n\\\nTu\"]],\"start1\":7648,\"start2\":7648,\"length1\":33,\"length2\":8},{\"diffs\":[[0,\"e paper.\"],[1,\"\\\n \\\n ## Encoding monomorphic and polymorphic types\\\n Explores the idea of monotonicity that is given in _Sort It Out..._ further, defining various new translations from monomorphic to untyped FOL (and polymorphic to monomorphic to untyped FOL?). In summary, it defines:\\\n \\\n  - Monomorphic lightweight tags (~t?) - this is like traditional tags but omitted for monotonic variables\\\n  - Monomorphic featherweight tags (~t??) - like lightweight tags, but omitted for monotonic variables and in cases where a tag can be safely omitted\\\n\\t  - \\\"if a universal variable does not occur naked in a formula, its tag can be safely omitted\\\"\\\n\\t  - this adds a few typing axioms as well\\\n  - Monomorphic lightweight guards (~g?) - like traditional guards but modified similarly to lightweight tags\\\n  - Monomorphic featherweight guards (~g??) - as above for featherweight tags\"],[0,\"\\\n\\\n## Arc\"]],\"start1\":10864,\"start2\":10864,\"length1\":16,\"length2\":869},{\"diffs\":[[0,\"ion.\\\n\\\n##\"],[1,\" (old)\"],[0,\" *Encodi\"]],\"start1\":11877,\"start2\":11877,\"length1\":16,\"length2\":22}]"
metadata_diff: {"new":{},"deleted":[]}
encryption_cipher_text: 
encryption_applied: 0
updated_time: 2023-10-02T12:37:23.412Z
created_time: 2023-10-02T12:37:23.412Z
type_: 13