- Idris is a purely functional programming language, with first class types - meaning that types are first class language constructs, and can be computed, stored in variables, passed to and returned from functions, just like any other first class construct.
- sounded too good to be true, and might still be viable, but I just came across an explicit desciription of negation in the language and even though they differentiate void and absurd (interesting), there is no room for dialectics it appears. But then again, I should probably not keep my hopes up to ever find somethign like that.
- Edwin Brady - Idris 2 - Type-driven Development of Idris
- https://www.tei-c.org/release/doc/tei-p5-doc/en/html/NH.html
- https://pdf.sciencedirectassets.com/272990/1-s2.0-S1571066108X03263/1-s2.0-S1571066108000200/main.pdf?X-Amz-Security-Token=IQoJb3JpZ2luX2VjENz%2F%2F%2F%2F%2F%2F%2F%2F%2F%2FwEaCXVzLWVhc3QtMSJIMEYCIQCbplAJO0MiwjM1LTMSuXnlp%2FsIIrGl8CvfYIfThKgjDQIhAOBmfJ9yRld%2BCK0%2Fr3yI2CyCh0dbpQ6YGUjmAHGZO86NKrQDCGQQAxoMMDU5MDAzNTQ2ODY1IgwZ9GlwjV1ZK6xSCyQqkQPN9WbeDl6eGLB5GgAnVDYZwafHetyyQV32b0jcaRCRPSafR2wbo3OM7zq2J19SXtuR8EMC%2Bvl3lyvdijls2Yp5MpC%2FIO%2F8l9smCA6zDM8fI3SEVV9tgyjhhBalvp%2FAUoQiIFBmRUNqCURDgq1swbOq4Lnh0Avhh64F63mMFofwmA3sJJQuIJJZGoHy8PxMvIw%2FHpxiGjnnKnquWQ8VkWPyedruu36OytfcPevGub%2F2CSA%2FgOxSrhcCkJBFqs5Ywv5%2Bam2Zit5ThX4qSTq84FRbiOXpr75mR4DUppJvcHme2VvqTurVJkJ%2FjvrrMEI7dJJiUPzH2NYUEwYfH4fE8UrMk4Oi11VdmGdPBjZPaGvKQOkkpsQR25p4tMWYYOwapaowWRvvcquwKlhP2ek3Q7jFU5RojqUpJAMnnwsMryzP3h%2Bp71SoKTmbSDU4TjknDneKkxQYMLFiffX476%2F9IWawPAceeAUP5xUsnj2eqjw0MXXZlyci7szDB6uLQBUc5U8kil4nnp69HLrUKNEpuw82tTDJg8T3BTrqAaqfqvAa592jyTUuUZ%2BJgv9BirC0ft6FcasbKVC%2BH1kRu82YZPyQZeWih%2BEYgDHFmthjGAw5WmDOXL7mQESlIn67c%2BMu41pRV5ys0izdaenjQ%2F%2FUXn4q8ITmqjwCofxcLl%2FKwhdDnHRlfQiyO7lLnJaqBHxrAvfM52F9Up1cEqdZ3TfCI%2FNjKh%2Ff63rWgDWcYtYP3WT2DjSgw5GNY0w%2FOJXj5A3n4VT51LTeiGdi4XXFVEO4wRXjfGA9IR52e66TeCQDgxoqf8uecvxiDaS8OHYYHcFnuAQ0MPfgxwyisUZ9XncWijok70BPcw%3D%3D&X-Amz-Algorithm=AWS4-HMAC-SHA256&X-Amz-Date=20200622T202917Z&X-Amz-SignedHeaders=host&X-Amz-Expires=299&X-Amz-Credential=ASIAQ3PHCVTYQZH5XA6A%2F20200622%2Fus-east-1%2Fs3%2Faws4_request&X-Amz-Signature=38d9aa587575fbb038034a528f5598169caff4a831fb0c43e01888fd24b612fe&hash=c74e881bb4fee5ff171e5a72455409f76df3c7049849ef90fddd0f32a4866afe&host=68042c943591013ac2b2430a89b270f6af2c76d8dfd086a07176afe7c76c2c61&pii=S1571066108000200&tid=spdf-62f93547-fb06-401a-9f4c-1901a310055a&sid=a9cc28b480c7e549d73b76a7359dd2567a63gxrqb&type=client