Tenth Post

I started work on the assignment again today. I have had lots of funky ideas about where I could take the project but I have realized that I don't have enough time and I am this close to finishing school so I'm going to stick to the original plan and finish it quickly. All the wack stuff I've been thinking about can be done in like the 5 month holiday I have before uni starts, and presumably then as well.

So I did this and got the lexer, parser and executer done to handle ml algebraic data types. The only thing I have to finish is the semantics checking stuff which I imagine might be a bit of a hassle but that's pretty much it.

Although I do want to keep it simple I do have some ideas for optional stuff that I can do if I have the time before the presentation.

That logic programming thing non-deterministic programming idea I had makes more sense the longer I think about it. 

I have simplified the type definitions a fair bit so it would be good to enforce recursive types. Like data list = cons[a, list] | end; only allowing a list type to be added in the second half of the cons would be good. Although this isn't strictly necessary for what I am doing right now. This is probably the first thing I will add if I have the time.

I have also thought about more advanced type theories still which would be neat. I also think it would be really impressive to have written my own type theory and be able to wack up a slide with like the sequent definitions or something. I have also thought of how I could build to it in the talk. Like I could be all "something this language is glaringly missing is higher-order functions. This isn't a practical problem, chucking functions on the data stack wouldn't be a problem at all in fact. The real issue is guaranteeing termination of the higher-order functions. As we can see from you know, the y-combinator (and the halting problem as a whole) we have to be very careful about constructing stuff. Also, allowing higher-order functions would allow us to use church encoded values, leaving behind the primitive data constructors used here (primitive is sarcastic). Something nifty about this is I just so happened to have written my own type theory for church encodings. I have not implemented it just yet because it's a little complicated (flip-up my sick maths slide here) and it doesn't *guarantee* termination just yet but I am working on it.". I just think that moment would be incredibly satisfying to me. I feel I haven't really had a chance to show off all the cool stuff I've been doing lately and this feels like the perfect opportunity.

Building out stdlib would be cool. I think one of the most fun things to do with a programming language I made is to write a sorting algorithm. so doing this would be quite nice.

That also brings me to the other thing I really need to do. Which is to implement if in the stdlib. The problem with the if function is that it takes booleans (which I didn't have until now) and that it requires some form of modified evaluation to not recurse infinitely (although this might not be a problem with the primitive recursion? I haven't really thought about it until now). 

Anyway, those are the ideas I have about where to go with this project right now and what needs to be done. I am optimistic about the future and am having a great time with the assigmment.

Comments

Post a Comment

Popular posts from this blog

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 ...
Read more

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