Add tutorials on Curry-Howard Isomorphism

melvic-ybanez / chi

A function code generator and an isomorphism analyzer

MIT License

37 stars 1 forks source link

Add tutorials on Curry-Howard Isomorphism #52

Open melvic-ybanez opened 2 years ago

melvic-ybanez commented 2 years ago

The following should also contain some common isomorphisms and code samples from supported languages. The user should be able to select which language to choose for the samples.

mlliarm commented 1 year ago

Hello,

Not exactly a tutorial, but this talk of prof. P. Wadler is an amazing introduction to the Curry-Howard Isomorphism.

If you want I can write a summary of the ideas mentioned there.

Regarding the common isomorphisms and code samples I'll have to do further research.

Overall really interesting enhancement, I'd love to work on this.

Cheers !

ps: Also these two talks of prof. Wadler [1][2] are very interesting as well, if you haven't watched them before. And finally, this paper [3] of prof. Baez is a must read, if only to keep the final result, the table with all the isomorphisms between the scientific fields mentioned there, that I believe is related to the Curry-Howard isomorphism.

[1] YouTube: "Everything Old is New Again: Quoted Domain Specific Languages"

[2] YouTube: "Categories for the Working Hacker"

[3] Arxiv.org: Physics, Topology, Logic and Computation: A Rosetta Stone

melvic-ybanez commented 1 year ago

Not exactly a tutorial, but this talk of prof. P. Wadler is an amazing introduction to the Curry-Howard Isomorphism.

Yes, I've watched this one before. It may actually be one of the resources I used to learn Curry-Howard Isomorphism. It's really useful.

@mlliarm I'd really appreciate it if you would work on this. It's good to see other people also interested in these topics.

Thanks for the links. I think I've only watched the second one.

mlliarm commented 1 year ago

I'd love to, @melvic-ybanez ! Thank you for creating such an interesting project !

Feel free to assign this issue to me.

If I write the tutorial/notes of the talk (and perhaps the basic ideas from Howards' paper) in Markdown, would it be okay?

Cheers !

melvic-ybanez commented 1 year ago

The plan is to eventually add the tutorial to the UI. So users can select a Tutorial menu item and see a new panel of explanations and examples. However, we can also have a separate task for that.

For now, it's okay to write it in Markdown, unless you also want to write the UI. I'm also open to other suggestions.

mlliarm commented 1 year ago

@melvic-ybanez I'll start with the Markdown and when time comes I can help with the UI, but will need some help to get started (like directions etc), because I don't know much about UI development. Thanks again.

mlliarm commented 1 year ago

Sorry, I got distracted from work and stuff. I'll start this week, but could take a while to have something complete.

As step 1: extract related notes from the talk of prof. Wadler on the CH-isomorphism.
As step 2: check Howard's paper and do a summary of the main ideas and arguments.
As step 3: create more examples in code in some static typed functional languages (I'll start with the ones you've already used).

Edit: Actually, that speech is based on this paper (PDF) of prof. Wadler. I'll start from here.

melvic-ybanez commented 1 year ago

No worries @mlliarm! The steps look good to me. Thanks for taking this one.