Posts

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

Eleventh post

Image
This week I made the semantics checkers. Normally when I write programming languages and code generally, I don't really care about errors or anything like that. This is the first time I have ever written any semantics checking and I feel proud of myself for doing it. My programming language feels so much more professional with compilation errors and everything like that. It is cool and I am having fun.  I did most of that stuff Monday and Tuesday of last week. I then tried to start working on the presentation and I wanted to write an example of how the non-determinism worked. Although the first example I tried pointed out the glaring flaw in my initial idea. Basically, the problem is that we rely on how fast something runs to delete branches and the like. As we have tried to sidestep the halting problem, we are making guesses that aren't true. The other way you could think about the problem is that a function running forever and a function running normally is indistinguishable ...

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

Ninth Post

 I have not worked on my assignment this week. I have been busy with physics and a new job thing I'm doing. I think I will probably just stick to the original plan, with the ml Esque algebra and the simple type checker. This is because I am new to type checkers so I do want to keep it simple. The type idea I had before is a good one but I don't know if I will have the time to fully develop it before the assignment is due. I think I will have to work through this fairly quick so I'll stick to the original plan.  I will continue to develop the idea in my own time though, just for fun. 

Eighth post

I took a break from I.T for a bit in the last week. I am trying to catch up on other assignments I have missed.  Although one thing I have been doing in my off hours is learning coq, and I think I understand structural recursion. It is basically what I tried to do before except sightly better described and works. So I think I'll probably just implement that. It seems to be pretty elegant.

Seventh Post

Ok, So I have calmed down from last weeks post. I thought about it and it wasn't as cool as I initially hoped, but I think it's still an idea worth pursuing. I did start pursuing it and read a lot about lots of different things. I have come to the conclusion that it's probably a form of dependent typing. I have not yet found the idea replicated anywhere but I am definitely thinking it's probably some weird subset of a pre-existing theory. I think it is also probably related to recursive typing. One last thing is that it appears to not really hold all that much extra power in the realms of normal typing algorithms, but I have had fun with it. The overall summary (just in case last weeks post was a bit too scatterbrained) is that I think we could enhance simply typed lambda calculus where instead of having variables (a -> a, a is the variable) in the type, we can create a way of describing acceptable inputs to the function. We can do this using context-free grammar (cf...

Sixth Post

 Ok so I read through the original paper on total functional programming and had a great time. Although it ended up not telling em about primtive recursion (a little bit but not enough to write into my language) and the most significant thing was that it linked back to the original hilbert recursion paper.  I haven't read the hilber recursion paper as of yet because I have had enormous problems getting my hands on it. It's on springerlink and springerlink is busted and I can't pirate it because it's not well known enough to pirate.  Though after intense frustration that my one good lead led back to the same paper, I asked my sister for help and she showed me how to get it ezpz through google scholar. I then started reading the paper and got a little bored (it's very densely written) so I started daydreaming about the potential type system I might have. This led to a series of very fun and interesting ideas that I am too excited about to finish the primitive recursio...