search

steshaw / plt

Programming Language Theory λΠ
https://steshaw.org/plt/
5.24k stars 340 forks source link

Fixes link to lambda-the-ultimate #6

Closed philippbayer closed 9 years ago

philippbayer commented 9 years ago

There's a "b" in missing in the link to Lambda the Ultimate, this adds it

steshaw commented 9 years ago

Thank you!

philippbayer commented 9 years ago

No worries! Now that I see it, I think the link to [Archives of Lambda the Ultimate] is mistaken too? It is the same link as for [Programming Language People]

steshaw commented 9 years ago

Ah, yeah, so it is. Now, I'm going to have to work out where that was supposed to point to :)

philippbayer commented 9 years ago

Possibly it's this one since it's the same URL as the switched link? http://www.angelfire.com/tx4/cus/lambdasort.html

steshaw commented 9 years ago

I think I've fixed it. See what you think!

philippbayer commented 9 years ago

Great, thank you :neckbeard:

steshaw commented 9 years ago

Thank you — I used a url almost the same as the one you found http://www.angelfire.com/tx4/cus/lambda.html. I think it's just sorted differently.

steshaw commented 9 years ago

@philippbayer, would you mind casting your eye over https://github.com/triplet-src/triplet-src.github.io? I'm not even sure if it makes sense :P

steshaw commented 9 years ago

Some of the Org(-mode) is better rendered at http://triplet-src.github.io/

philippbayer commented 9 years ago

I was wondering what the [fn:2] meant :)

For now, I think it's just not detailed enough - I have very little background in logic and I had to read through all the given links, would it be possible to find very short "generic"/"laymen" English descriptions for some of the points?

Like, "We plan to design and implement a programming language based on the Univalent Foundations (a relatively new area of research trying to reconnect "pure mathematics" and theory of computation and theory of programming languages)"

Do you have any extremely simple examples? Just "this is what the final language should do or could do" - or even a FAQ? I know it's an extremely hard thing to do for such an ambitious goal...

steshaw commented 9 years ago

Thanks, @philippbayer, I'll take you comments onboard! It's early days on this, I haven't really started anything yet except trying to get back into learning HoTT via Robert Harper's CMU lecture series on it. Further details including a FAQ will come as folks join—perhaps even if they don't ;). It took me a surprisingly long time to put together this simple, short page.

I'm just a frustrated dreamer looking for a University—someone—to teach me TT/PT/CT and all those kinds of things but coming up short (without moving a long way which I'm unable to do for a few years due to family reasons).

Oh, and I have no idea what the language should look like or how it will be different to existing languages. Haskell and Idris are already terrific, as are many in the ML Family. I hope it's possible to integrate the HoTT ideas into an existing language somehow—I'd certainly like to leverage something! That language will likely be Idris since it has full dependent types already.

I'd also like to see an ML module system for Idris under the auspices of the Triplet SRC. I know that @edwinb isn't interested in module systems but he might let me try to build one…

edwinb commented 9 years ago

I am interested in module systems, but there's only so many things I can think about at once... lots of people have suggested Idris should have one, but nobody so far has stepped up and actually offered one. If anyone does, or even if anyone has a well thought out design, that's a great start!

steshaw commented 9 years ago

Careful, @edwinb, I'm starting to get excited! I'd love to try 'n' bring a module system to Idris. I'll need help. Would you be happy to take me on as a mentee? A kind of unofficial graduate student?

I would hope to find more help. It's possible that @RobertHarper might want to help me out with some pointers at least. He showed some interest a while ago on twitter.