tuplas - programas hechos en haskell

Haskell: ejemplo de función de tipo a-> a, además de la identidad

Question

Acabo de empezar a jugar un poco con Haskell ... Quiero escribir una función del mismo tipo de identidad. Obviamente, no es equivalente a ello. Eso sería algo así como,

myfunction :: a -> a

No puedo dar un ejemplo en el que el parámetro y el tipo de retorno sean los mismos y puedan ser prácticamente cualquier cosa (esto excluye la posibilidad de usar las Clases de tipos de Haskell).

Answer 1

A menos que esté dispuesto a usar undefined o bottom (una expresión sin terminación), literalmente no hay otras funciones que satisfagan ese tipo.

Esta es una de las grandes fortalezas del sistema tipo Haskell. Es posible limitar fuertemente las posibles funciones que pueden pasar de un compilador a las que obviamente son correctas. Para un ejemplo extremo, vea djinn - toma un tipo y genera posibles funciones que coinciden con ese tipo. Incluso para ejemplos reales y complejos, la lista es a menudo muy corta.

Answer 2

Como han mencionado otros, no puede existir ninguna otra función total . (Si no nos limitamos a funciones totales, entonces podemos habitar cualquier tipo por undefined ).

Intentaré dar una explicación teórica basada en el cálculo λ:

Para simplificar, limitémonos a los términos λ (a los que podemos traducir cualquier expresión de Haskell). Para un término λ M llamemos a A su cabecera si M ≡ A N1 ... Nk y A no es una aplicación ( k también puede ser cero). Tenga en cuenta que si M está en forma normal , A no puede ser una abstracción λ a menos que k = 0 .

Entonces, M :: a -> a es un término λ en forma normal. Como no tenemos variables en el contexto, M no puede ser una variable y no puede ser una aplicación. Si lo fuera, su cabeza tendría que ser una variable. Entonces, M debe ser una abstracción λ, debe ser M ≡ λ(x:a).N .

Ahora N debe ser de tipo a , formalmente {x:a}⊢N:a . Si N era una abstracción λ, su tipo sería σ -> τ , lo cual no es posible. Si N era una aplicación de función, entonces su cabecera tendría que ser una variable, y la única que tenemos en el contexto es x . Pero como x:a , no podemos aplicar x a nada, x P no se puede marcar para ninguna P. Entonces, la única posibilidad es que N ≡ x . Entonces, M debe ser λ(x:a).x .

_{(Por favor corrija mi inglés, si es posible. En particular, no estoy seguro de cómo usar el derecho de subjunctive ).}

Answer 3

Esto es imposible sin usar undefined como mencionó otro comentarista. Vamos a demostrarlo por contra-ejemplo. Supongamos que existía tal función:

f :: a -> a

Cuando dices que no es lo mismo que id , eso implica que no puedes definir:

f x = x

Sin embargo, considere el caso donde a es el tipo () :

f () = ...

El único resultado posible que f podría devolver sería () , pero esa sería la misma implementación que id , por lo tanto, una contradicción.

La respuesta más sofisticada y rigurosa es mostrar que el tipo a -> a debe ser isomorfo a () . Cuando decimos que dos tipos a y b son isomorfos, eso significa que podemos definir dos funciones:

fw :: a -> b
bw :: b -> a

... tal que

fw . bw = id
bw . fw = id

Podemos hacer esto fácilmente cuando el primer tipo es a -> a el segundo tipo es () :

fw :: (forall a . a -> a) -> ()
fw f = f ()
bw :: () -> (forall a . a -> a)
bw () x = x

Entonces podemos probar que:

fw . bw
= /() -> fw (bw ())
= /() -> fw (/x -> x)
= /() -> (/x -> x) ()
= /() -> ()
= id
bw . fw
= /f -> bw (fw f)
-- For this to type-check, the type of (fw f) must be ()
-- Therefore, f must be `id`
= /f -> id
= /f -> f
= id

Cuando demuestras que dos tipos son isomorfos, una cosa que sabes es que si un tipo está habitado por un número finito de elementos, el otro también debe hacerlo. Dado que el tipo () está habitado exactamente por un valor:

data () = ()

Eso significa que el tipo (forall a . a -> a) también debe estar habitado por exactamente un valor, que resulta ser la implementación de id .

Edit: Algunas personas han comentado que la prueba del isomorfismo no es lo suficientemente rigurosa, por lo que invocaré el lema de Yoneda, que cuando se traduce a Haskell, dice que para cualquier función f :

(forall b . (a -> b) -> f b) ~ f a

Donde ~ significa que (forall b . (a -> b) -> fb) es isomorfo a fa . Si elige el functor de Identity , esto se simplifica a:

(forall b . (a -> b) -> b) ~ a

... y si elige a = () , esto se simplifica aún más a:

(forall b . (() -> b) -> b) ~ ()

Puedes probar fácilmente que () -> b es isomorfo a b :

fw :: (() -> b) -> b
fw f = f ()
bw :: b -> (() -> b)
bw b = /() -> b
fw . bw
= /b -> fw (bw b)
= /b -> fw (/() -> b)
= /b -> (/() -> b) ()
= /b -> b
= id
bw . fw
= /f -> bw (fw f)
= /f -> bw (f ())
= /f -> /() -> f ()
= /f -> f
= id

Entonces podemos usar eso para finalmente especializar el isomorfismo de Yoneda para:

(forall b . b -> b) ~ ()

Lo que dice que cualquier función de tipo para todo forall b . b -> b forall b . b -> b es isomorfo a () . El lema de Yoneda proporciona el rigor de que faltaba mi prueba.

Answer 4

La clave aquí es entender que no sabemos nada acerca de a , especialmente no tenemos manera de generar una nueva o de transformarla en algo diferente. Por lo tanto, no tenemos otra opción como devolverlo (o el valor inferior). Tan pronto como tengamos más información acerca de a (por ejemplo, un límite de contexto), podemos hacer más cosas interesantes con él:

f :: Monoid a => a -> a
f _ = mempty

o

f :: Monoid a => a -> a
f x = x `mappend` x `mappend` x

O si tiene la opción como en f :: (a, a) -> a , tiene dos implementaciones posibles (ignorando los valores inferiores nuevamente), pero para f :: (a, b) -> a está de nuevo en una implementación, que es la misma que para fst : Si bien es válido llamar a f con un par de tipos idénticos, por ejemplo, f ("x", "y") , puede estar seguro de que f comporta como fst , porque en la la implementación de f no tiene manera de probar si ambos tipos de argumentos podrían ser iguales. De manera similar, solo hay una versión no inferior de f :: (a -> b) -> a -> b .

El polimorfismo limita los grados de libertad, porque no sabes nada acerca de tus argumentos, y en algunos casos se reduce a una versión sin fondo.

Answer 5

Permítame formular una respuesta que explique el comentario de dbaupp. Cualquier función de tipo a -> a también daría lugar a una función de type () -> () , así que primero veré este subproblema.

Una semántica habitual de los tipos y funciones de Haskell representaría un tipo como un orden parcial de cadena puntiaguda completa y funciona como funciones continuas. El tipo () está representado por el conjunto de dos elementos {⊥, ()} con el orden ⊥⊏ () . En la teoría de conjuntos lisos, hay 2 ^ 2 = 4 funciones de este conjunto en sí mismo, pero solo tres de ellas son continuas:

• f1: ⊥ ↦ ⊥, () ↦ ⊥,
• f2: ⊥ ↦ ⊥, () ↦ (), y
• f3: ⊥ ↦ (), () ↦ ().

Entonces, en nuestro modelo semántico, hay tres funciones diferentes de type () -> () . ¿Pero cuál de ellos se puede implementar en Haskell? ¡Todos ellos!

• f1 _ = undefined (o f1 x = f1 x )
• f2 x = x (o f2 = id )
• f3 _ = () (o f3 = const () )

Al observar estas definiciones, puede ver que f1 y f2 también se pueden usar para definir una función de tipo a -> a . Como hacen cosas diferentes ya en () , son diferentes. Entonces tenemos al menos dos funciones diferentes de tipo a -> a .

En el modelo semántico anterior, hay muchas más funciones de tipo a -> a , pero estas no se podrían expresar en Haskell (esto está relacionado con la parametricidad y los teoremas de Wadler para libre ). Una prueba adecuada de que f1 y f2 son las únicas funciones de este tipo no parece ser muy fácil, ya que depende de lo que el lenguaje Haskell no permita (por ejemplo, no hay coincidencia de patrones en el tipo de argumento).