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 recursion checker. I will come back and finish it but for now, I am going to do this idea because it is very cool.

(also if you are reading this as a type theorist or mathematician or whatever and are thinking "this guy doesn't know what he's talking about. This is clearly just reinventing riff-raff type theory or whatever please keep in mind that I'm new to type theory and it is really late at night rn).

I will now recount my thought process in thinking about this.

1. Wouldn't it be really cool if instead of having like ml-type type algebra we could do like a minimalist type system with higher order functions and natural numbers, but using church encoding to encode data structures (like cons lists or whatever). Might be cool to have a type alias system. Like List = [some type] or whatever.

2. This would be really easy to implement in the original system as well because if the passed function is primitive then no matter how we use it, it should still be primitive. Something kinda weird that I need to think about is that passing a function to itself would produce an infinte type signature. Oh and the church-encoded values will have different type signatures depending on their value.

3. I need a way to allow for more complex type signatures to be handled elegantly by the type system. (also the same problem applies to mutual recursion with passing your parameter back and forth).

4. The only problem I'm having now is infinite recursion but I can think about this later.

5. It's hard to write a type when the thing's type you are trying to define changes depending on it's value. Also to handle functions calling itself with a parameter passed with itself could be handled by introducing a Rec type, which means a recursive dtype definition on itself (ok I know recursive type signatures are real, I just haven't looked into them yet and are making an educated guess).

6. I might be able to use the type alias to define a type or whatever. Like we can say that a list's type signature is x | (x -> rec -> rec) -> rec (where x is a natural number / terminal / maybe generic value for all. And rec is a recursive type signature. | is or, like in bnf. 

7. Something important about this is type checking a single argument has become linear time. I think it's rad enough to move forward but it is another knock against the real-world value I am bringing. I was thinking that I might be able to define a natural number as, instead of a type signature, as the return value of a function, or a function that calls that original function, and so on. 

8. I feel like this is getting closer to tagged unions but I will forge onwards alas. 

9. Another possible implementation is that the above type alias definition kinda looks like a cfg. and I have been mostly describing the type system syntactically. Potentially I just full on embrace the cfg and define types by cfg.

10. Maybe I can just implement this cool type system as another language. Then after having to think about and deal with this type system for a while, we bring it back and try to re-integrate it with the other language. 

11. Maybe even just keep them separate as two cool proof of concept programming languages.

[side note / tangent] is this what dependent type theory is or am I tripping?

[side note / tangent] could we write polyprimitive functions. Like a function that can be passed primtiive or non primitive functions and it all handles the same. Like compose could be done like this

[side note / tangent] i have avoided the thought so far but how do we test functions for infinite recursion? Cause if we just assume that all function calls are primitive recursive and the only time we need to worry is if we have natural numbers (or on that point if we church encode numerals as well) then that's blatantly not true. We can do the fixed point combinator in this system and it seems like we have side-stepped the whole mathematical need for a type system (like stlc was invented to avoid the y combinator or whatever). I plan to check this out tomorrow by looking at how stlc handles church encoded numeralsd. This is the only problem for the idea as of right now, I will check back again tomorrow to see how it went. 

edit1: I have woken up tomorrow and took a look back at what I did yesterday and I must say it's still pretty cool. I have also woken up suddenly able to understand type theories and so have worked through a few type theories to get an understanding of how other type systems work. This is still very much in progress and maybe a bad idea but I will continue working on it until I can get a real definition down.

edit2.1: After more thought with a fresh mind I realized that I had spontaneously forgotten how type definitions work yesterday. The type for natural numbers is forall a. (a -> a) -> a -> a. Why did I think something else?

edit2.2: This doesn't mean what I thought of was bad. I think what I can still do is define types by cfg on the actual value of the element, rather than the type. I think this is what I was trying to write about yesterday but just didn't. 

edit2.3: So I think I might be able do something a little funky here and am excited for it!

edit2.4: the advantage of this over stlc is that the type's can be actually meaningful. In stlc (and system f) we do kind of know what happens with each thing but, at least in church encoding, it is really hard to tell the difference between like a number or just a function that shares the type signature. Using a cfg on lambda terms to type check values is like super cool because we can now distinguish between these two things. Although we have suddenly, massively increased time complexity, it is still cool.

edit2.5: so I am considering it but this sounds like the most fun thing to do, and the other project was basically finished, all I needed was like a small change to the primtive recursion definition then adding all the boring ml type algebra stuff. 

edit3: I have emailed Mr Griffin about doing two projects and he has yet to get back to me. For now, I will properly define how this cfg system works and start implementing it. I hope to be able to get this system done by yicte so that I can show off two programming languages. Also for yicte it is not really that important that my definition of primitive recursive isn't 100% accurate because it's not really the point of the language and the point still gets across.

edit4: kinda lame that type checking has to run at run time because it depends on the value. 

edit5: I did look into dependent types and I am pretty sure they're not too applicable, but they very well could be. Maybe this is a form of dependent typing, maybe I need to read about the calculus of constructions.