Fifth post

 This week I was reading a bit about maths and other things and discovered that my approach to primitive recursion has already been done. It is called structural recursion https://en.wikipedia.org/wiki/Structural_induction. (this is about my definition of primitive recursion, not the integration. Also as a side note, I am using primitive recursion in place of terminating recursion because I am lazy with my terminology, I apologize).


I also realized that my project wasn't that interesting and that my type system especially was kinda lame. I feel as if I can go harder and make my type system more interesting and worth doing. I also feel that the amount of time I've given myself too much time so I'll end up not really doing much for most of it. Due to these reasons, I have been exploring some type theories to see if there's anything I can mangle into a type system for this assignment. 


The main candidates (so far, this is early days of research) are:

- Hindley Milner

- not because it's particularly challenging, but because of the legacy. Although this is why I am considering not doing it.

- Calculus of constructions

- this would be good because I know that it works in a programming language well (coq). 

- It also is good because it's something interesting and new to me so I won't get bored.

- Although as it has already been implemented some of the appeal is lost.

- Homotopy type theory

- I have no idea how it works or how intuitionistic type theory works so I really need to do my research.

- This is the first maths field I have discovered that is actively being researched so the appeal is very high

- (hopefully) nobody has done this yet?

- I am very uncertain on how to apply it to programming languages.

- This is the front runner for me because of how cool it is but it will require some serious reading.

and if this idea falls through and it turns out type theory is not fun then I can always fall back on the super simple type system I was planning on implementing at the start. But so far I have had a lot of fun with it.


Something that I need to consider is how this type system will interact with the integration. The integration is specified with the bottom type in theory but I may have accidentally written myself into a hole here because no function can return the bottom type or something. Either way, I need to get a type system that will handle this oddity or change to returning the unit type, but this is also another issue so I am unsure. Further research is definitely needed.


In terms of challenges this week, learning maths outside of school is always going to be a little hard but it's why I am doing it. It's a fun challenge. On top of this, I am having problems with the relationships between type theory and first-order logic. I am also having a really hard time understanding Curry-Howard correspondence which I think is going to probably be pretty important for a project like this. But I assume this is just a lack of understanding of type theory (and logic) which is holding me back so hopefully by the time I have to begin development on the type system (and fixing the old primitive checker) I will have figured it out. Or potentially get someone to explain it to me.

Comments

Post a Comment

Popular posts from this blog

Twelfth post (end post)

This is the conclusion of the project. As I write this I have completely finished the language to where I wanted it to be. I am very happy with how it turned out. I am currently trying to describe the project mathematically and write a proof that the non-deterministic execution environment that I wrote does in fact halt.  It was fun to work on a long-form project like this, I have never done something as massive as this before and it was cool to do. I think I got to 1.2k lines which doesn't sound like much but it is 1.2k lines of some serious thinking. Not a lot of filler code in the project. On that note I did really have to think hard creating this, there were a lot of algorithms that I didn't have the time to read about and learn so I had to write them myself. It was challenging and very fun.  I think at the start of this project I didn't really have the strongest grasp on the areas I was talking about, but as time has gone on, especially lately, I have come to really un...
Read more

Fourth Post

I did a little bit of commenting and added a tutorial to make the project suitable to submit. During this I discovered a problem with my defininition of primitive functions, but it is too late to fix before the prototype is due. I am planning to update the defintion to probably just be the primitive functions, although I am considering two alternatives, substructural or hilbert recursion. I then submitted the project and will do no further work for a few weeks while I catch up on other assignments. note: I did miss last weeks blog post and probably did the work listed above then, it's hard to remember, it's been very hectic. Sorry I'll try to stick closer to the one post a week format from now on.
Read more