simbolos - ¿Por qué no se permite la definición de funciones para todos los tipos a la vez en Haskell?

hola mundo en haskell

Question

Esta es probablemente una pregunta muy básica, pero ...

Una función que se define como, por ejemplo

foo :: a -> Integer

denota una función de cualquier tipo a un Entero. Si es así, entonces, en teoría, uno debería ser capaz de definirlo para cualquier tipo, como por ejemplo

foo 1 = 10
foo 5.3 = 100
foo (x:xs) = -1
foo _ = 0

Pero Haskell solo permite una definición general, como foo a = 0 .

E incluso si restringe a ser uno de una cierta clase de tipos, como una instancia de la clase de tipo Show:

foo :: (Show a) => a -> Integer

todavía no puedes hacer algo como

foo "hello" = 10
foo _ = 0

aunque "hello" :: [Char] es una instancia de Show

¿Por qué hay tal restricción?

Answer 1

¡Esta pregunta se basa en una premisa errónea, Haskell puede hacer eso! (aunque generalmente solo se usa en circunstancias muy específicas)

{-# LANGUAGE ScopedTypeVariables, NoMonomorphismRestriction #-}
import Data.Generics
q1 :: Typeable a => a -> Int
q1 = mkQ 0 (/s -> if s == "aString" then 100 else 0)
q2 :: Typeable a => a -> Int
q2 = extQ q1 (/(f :: Float) -> round f)

Cargue esto y experimente con él:

Prelude Data.Generics> q2 "foo"
0
Prelude Data.Generics> q2 "aString"
100
Prelude Data.Generics> q2 (10.1 :: Float)
10

Esto no necesariamente entra en conflicto con las respuestas que afirman que los tipos no tienen significado computacional. Esto se debe a que estos ejemplos requieren la restricción Typeable , que reifica los tipos en valores de datos a los que se puede acceder durante el tiempo de ejecución.

La mayoría de las llamadas funciones genéricas (por ejemplo, SYB) se basan en una Typeable o de Data . Algunos paquetes presentan sus propias funciones alternativas para servir esencialmente al mismo propósito. Sin algo como estas clases, no es posible hacer esto.

Answer 2

El tipo a -> Integer no significa realmente "función de ningún tipo a Integer " como lo está describiendo. Cuando una definición o expresión tiene a -> Integer tipo a -> Integer , significa que para cualquier tipo T , es posible especializar o crear una instancia de esta definición o expresión en una función de tipo T -> Integer .

Cambiando la notación ligeramente, una forma de pensar en esto es que foo :: forall a. a -> Integer foo :: forall a. a -> Integer es realmente una función de dos argumentos: un tipo a y un valor de ese tipo a . O, en términos de currying, foo :: forall a. a -> Integer foo :: forall a. a -> Integer es una función que toma un tipo T como su argumento, y produce una función especializada de tipo T -> Integer para ese T Usando la función de identidad como un ejemplo (la función que produce su argumento como resultado), podemos demostrar esto de la siguiente manera:

-- | The polymorphic identity function (not valid Haskell!)
id :: forall a. a -> a
id = /t -> /(x :: t) -> x

Esta idea de implementar el polimorfismo como un argumento de tipo para una función polimórfica proviene de un marco matemático llamado Sistema F , que Haskell realmente usa como una de sus fuentes teóricas. Sin embargo, Haskell oculta por completo la idea de pasar parámetros de tipo como argumentos a las funciones.

Answer 3

Es una característica, y en realidad es muy fundamental. Se reduce a una propiedad conocida como parametricidad en la teoría del lenguaje de programación. Aproximadamente, eso significa que la evaluación nunca debe depender de los tipos que son variables en tiempo de compilación. No puede ver un valor donde no se conoce su tipo concreto estáticamente.

¿Por qué es eso bueno? Proporciona invariantes mucho más fuertes sobre los programas. Por ejemplo, usted sabe por el tipo solo que a -> a tiene que ser la función de identidad (o diverge). "Teoremas libres" similares se aplican a muchas otras funciones polimórficas. La parametricidad también es la base para técnicas de abstracción basadas en el tipo más avanzadas. Por ejemplo, el tipo ST sa en Haskell (la mónada de estado) y el tipo de la función runST correspondiente, dependen de que s sea ​​paramétrica. Eso asegura que la función de ejecución no tiene forma de interferir con la representación interna del estado.

También es importante para una implementación eficiente. Un programa no tiene que pasar información de tipo costosa en tiempo de ejecución ( borrado de tipo ), y el compilador puede elegir representaciones superpuestas para diferentes tipos. Como ejemplo de esto último, 0 y False y () y [] están todos representados por 0 en el tiempo de ejecución. Esto no sería posible si se permitiera una función como la tuya.

Answer 4

Haskell disfruta de una estrategia de implementación conocida como "borrado de tipos": los tipos no tienen importancia computacional, por lo que el código que usted emite no necesita rastrearlos. Esto es una gran ayuda para el rendimiento.

El precio que paga por este beneficio de rendimiento es que los tipos no tienen importancia computacional: una función no puede cambiar su comportamiento en función del tipo de argumento que se transmite. Si permitieras algo como

f () = "foo"
f [] = "bar"

entonces esa propiedad no sería verdadera: el comportamiento de f dependería del tipo de su primer argumento.

Ciertamente, hay idiomas que permiten este tipo de cosas, especialmente en los idiomas de tipos dependientes donde los tipos generalmente no se pueden borrar de todos modos.

Answer 5

Para una función a -> Integer , solo hay un comportamiento permitido - devuelve un entero constante. ¿Por qué? Porque no tienes idea de qué tipo es a. Sin restricciones especificadas, podría ser absolutamente cualquier cosa, y como Haskell está tipado estáticamente, debe resolver todo lo relacionado con los tipos en tiempo de compilación. En tiempo de ejecución, la información de tipo ya no existe y, por lo tanto, no se puede consultar: ya se han realizado todas las elecciones de las funciones que se utilizarán.

Lo más cercano que Haskell permite a este tipo de comportamiento es el uso de clases de tipos, si creaste una clase de tipos llamada Foo con una función:

class Foo a where
foo :: a -> Integer

Entonces podrías definir instancias de él para diferentes tipos

instance Foo [a] where
foo [] = 0
foo (x:xs) = 1 + foo xs
instance Foo Float where
foo 5.2 = 10
foo _ = 100

Entonces, siempre que pueda garantizar que algún parámetro x es un Foo , puede llamar a foo en él. Sin embargo, aún necesitas eso; no puedes escribir una función

bar :: a -> Integer
bar x = 1 + foo x

Porque el compilador no sabe que a es una instancia de Foo . Tienes que decirlo, o dejar de lado la firma de tipo y dejar que lo resuelva por sí mismo.

bar :: Foo a => a -> Integer
bar x = 1 + foo x

Haskell solo puede operar con tanta información como el compilador tenga sobre el tipo de algo. Esto puede sonar restrictivo, pero en la práctica las clases de tipos y el polimorfismo paramétrico son tan poderosos que nunca dejo de escribir dinámicamente. De hecho, generalmente me resulta molesto el tipado dinámico, porque nunca estoy completamente seguro de qué es realmente.