search

libreim / blog

Blog colaborativo sobre matemáticas e informática de la comunidad de @libreim.
https://libreim.github.io/blog
GNU General Public License v3.0
29 stars 8 forks source link

Post teoria de tipos #108

Closed mroman42 closed 8 years ago

mroman42 commented 8 years ago

Un post de enlaces sobre teoría de tipos. Tratando álgebra, Curry-Howard, inducción estructural y parametricidad. Voy a intentar ampliarlo todavía un poco más, pero la idea final debe ser más o menos esta.

mroman42 commented 8 years ago

Por mi parte está listo para revisar.

mx-psi commented 8 years ago

Yo lo veo perfecto. Lo único que me genera algo de duda es el paper de Wadler del isomorfismo de Girald-Reynolds. Si el post tiene un enfoque introductorio a lo mejor ese paper es un poco hardcore y demasiado extenso y estaría bien tener algo previo que fuera más sencillo.

No lo he leído entero y me estoy basando más bien en lo que recuerdo de cuando nos explicó eso pero me da esa impresión (puede que errónea) de que es un poco complejo así de primeras.

andreshp commented 8 years ago

Genial! Iré leyendo la bibliografía que enlazas conforme pueda ^^

Creo que posts de este estilo pueden ser muy útiles y ayudan tanto al que quiera empezar como al que quiera profundizar en la temática.

mroman42 commented 8 years ago

Es verdad, me he pasado cuatro pueblos soltando ahí el Wadler, creo que tengo uno por ahí que explicaba muy sencillito el isomorfismo con Gentzen. El de Propositions as Types era el bueno ahí, creo que lo voy a poner y dejo el otro para ampliar.

¡Gracias, Pablo!

mroman42 commented 8 years ago

Gracias, Andrés. Sobre todo que son mucho más sensatos y cómodos de preparar que intentar volver a contar un camino que otros pueden explicar mucho mejor que yo.