Incrustar tipos de mayor kínder (¡mónadas!) En el cálculo lambda sin tipo

Question

Es posible codificar varios tipos en el cálculo lambda sin tipo a través de funciones de orden superior.

Examples: 
zero = λfx.  x 
one = λfx.  fx 
two = λfx. f(fx) 
three = λfx. f(f(fx)) 
etc 

true = λtf. t 
false = λtf. f 

tuple = λxyb. b x y 
null = λp. p (λxy. false) 

Me preguntaba si se ha investigado la incorporación de otros tipos menos convencionales. Sería genial si hay algún teorema que afirme que cualquier tipo puede ser incrustado. Tal vez haya restricciones, por ejemplo, solo se pueden incrustar tipos de tipo *.

Si es posible representar tipos menos convencionales, sería increíble ver un ejemplo. Estoy particularmente interesado en ver cómo son los miembros de la clase de tipo mónada.

Answer 1

Está mezclando el nivel de tipo con el nivel de valor. En el cálculo lambda sin tipo no hay mónadas. Puede haber operaciones monádicas (nivel de valor), pero no mónadas (nivel de tipo). Sin embargo, las operaciones en sí mismas pueden ser las mismas, por lo que no pierde ningún poder expresivo. Entonces, la pregunta en sí misma no tiene sentido.

Answer 2

Bueno, ya tenemos tuplas y booleanos, por lo tanto, podemos representar Either ya su vez cualquier tipo no recursivo suma basado en que:

type Either a b = (Bool, (a, b)) 
type Maybe a = Either() a 

y tal vez es miembro de la clase de tipo Mónada. La traducción a la notación lambda se deja como ejercicio.

Answer 3

Es posible representar casi cualquier tipo que desee. Pero como las operaciones monádicas se implementan de manera diferente para cada tipo, es no posible escribir >>= una vez y hacer que funcione para cada instancia.

Sin embargo, usted puede escribir funciones genéricas que dependen de pruebas de la instancia de la clase de tipos. Considere e aquí para ser una tupla, donde fst e contiene una definición de "enlace" y snd e contiene una definición de "retorno".

bind = λe. fst e -- after applying evidence, bind looks like λmf. ___ 
return = λe. snd e -- after applying evidence, return looks like λx. ___ 

fst = λt. t true 
snd = λt. t false 

-- join x = x >>= id 
join = λex. bind e x (λz. z) 

-- liftM f m1 = do { x1 <- m1; return (f x1) } 
-- m1 >>= \x1 -> return (f x1) 
liftM = λefm. bind e m (λx. return e (f x)) 

Debería entonces definir una "tupla de pruebas" para cada instancia de Monad. Tenga en cuenta que de la forma en que definimos bind y return: funcionan igual que los otros métodos Monad "genéricos" que hemos definido: primero se les debe dar evidencia de Monad-ness, y luego funcionan como se esperaba.

Podemos representar Maybe como una función que toma 2 entradas, la primera es una función para realizar si es Just x, y la segunda es un valor para reemplazarla si es Nada.

just = λxfz. f x 
nothing = λfz. z 

-- bind and return for maybes 
bindMaybe = λmf. m f nothing 
returnMaybe = just 

maybeMonadEvidence = tuple bindMaybe returnMaybe 

Las listas son similares, representan una lista como su función de plegado. Por lo tanto, una lista es una función que toma 2 entradas, una "contra" y una "vacía". A continuación, realiza foldr myCons myEmpty en la lista.

nil = λcz. z 
cons = λhtcz. c h (t c z) 

bindList = λmf. concat (map f m) 
returnList = λx. cons x nil 

listMonadEvidence = tuple bindList returnList 

-- concat = foldr (++) [] 
concat = λl. l append nil 

-- append xs ys = foldr (:) ys xs 
append = λxy. x cons y 

-- map f = foldr ((:) . f) [] 
map = λfl. l (λx. cons (f x)) nil 

Either es también sencillo. Representar un tipo cualquiera como una función que toma dos funciones: una para aplicar si es un Left, y otra para aplicar si es un Right.

left = λlfg. f l 
right = λrfg. g r 

-- Left l >>= f = Left l 
-- Right r >>= f = f r 
bindEither = λmf. m left f 
returnEither = right 

eitherMonadEvidence = tuple bindEither returnEither 

No se olvide, funciones mismos(a ->) forma una mónada. Y todo en el cálculo lambda es una función ... así que ... no lo pienses demasiado. ;) Inspirado directamente de la fuente de Control.Monad.Instances

-- f >>= k = \ r -> k (f r) r 
bindFunc = λfkr. k (f r) r 
-- return = const 
returnFunc = λxy. x 

funcMonadEvidence = tuple bindFunc returnFunc