Re: Abridged summary of functional-oriented-hackers-mvd@googlegroups.com - 1 Message in 1 Topic

[math]

Son tipos que están parametrizados en un tipo que no aparece en ellos (aparecer desaparecer jajaj no se entiende nada).

El ejemplo típico es el de la expresiones, con constructores como:

.+. :: Exp Int -> Exp Int -> Exp Int

.. 

.=. :: Exp Int -> Exp Int -> Exp Bool 

..

.or. :: Exp Bool -> Exp Bool -> Exp Bool 

Que son los Tipos Dependientes?

Salut

2011/5/2 <functional-oriented...@googlegroups.com>

  Today's Topic Summary

Group: http://groups.google.com/group/functional-oriented-hackers-mvd/topics

• Post-reunion links [1 Update]

 Topic: Post-reunion links

fedesilva <fede....@gmail.com> May 01 03:54PM -0700 ^
 
con Mathias nos quedamos hablando post-reunión de una variedad de cosas y el
me hablaba de phantom types.
 
Math acá va more...

[Bruno Martínez]

Math puso un GADT, otro bicho más complicado. Un tipo con phantom
type mas simple seria el de los campos de HList:

data Field label value = Field value

Ahí label no se usa pero sirve para diferenciar mediante el tipo dos
campos iguales:

data Height
data Weight

h :: Field Height Int
h = Field 180

w :: Field Weight Int
w = 80

Bruno

2011/5/2 math <mathias.e...@gmail.com>:

[math]

Si, es cierto..

(es un GADT con un phanton type?
o me dejo de phanton type?)

Otra cosa

append :: suma m n mn => Vec a m -> Vec a n -> Vec a mn

eso es un dependent type¿?


Saludos,
Mathias


pd: recien ahora vi que si respondo desde gmail como un mail al grupo
lo crea como un nuevo tema jaja mal yo..

On 3 mayo, 01:18, Bruno Martínez <bruno...@gmail.com> wrote:
> Math puso un GADT, otro bicho más complicado.  Un tipo con phantom
> type mas simple seria el de los campos de HList:
>
> data Field label value = Field value
>
> Ahí label no se usa pero sirve para diferenciar mediante el tipo dos
> campos iguales:
>
> data Height
> data Weight
>
> h :: Field Height Int
> h = Field 180
>
> w :: Field Weight Int
> w = 80
>
> Bruno
>

> 2011/5/2 math <mathias.etcheve...@gmail.com>:

>
>
>
>
>
>
>
> > Son tipos que están parametrizados en un tipo que no aparece en ellos
> > (aparecer desaparecer jajaj no se entiende nada).
> > El ejemplo típico es el de la expresiones, con constructores como:
> > .+. :: Exp Int -> Exp Int -> Exp Int
> > ..
> > .=. :: Exp Int -> Exp Int -> Exp Bool
> > ..
> > .or. :: Exp Bool -> Exp Bool -> Exp Bool
>
> > Que son los Tipos Dependientes?
> > Salut
> > 2011/5/2 <functional-oriented...@googlegroups.com>
>
> >>   Today's Topic Summary
>
> >> Group:
> >>http://groups.google.com/group/functional-oriented-hackers-mvd/topics
>
> >> Post-reunion links [1 Update]
>
> >>  Topic: Post-reunion links
>

> >> fedesilva <fede.si...@gmail.com> May 01 03:54PM -0700 ^

[Bruno Martínez]

Si, ese tipo de cosas son tipos dependientes. Obviamente, cualquier
tipo es dependiente, pero los interesanes son los que no podes
expresar en los lenguajes comunes.

Bruno

2011/5/2 math <mathias.e...@gmail.com>: