¿Existe alguna forma práctica de usar números naturales en Haskell?

Question

Estoy aprendiendo Haskell y me gustaría imponer el uso de enteros positivos (1,2,3, ...) en algunos constructores, pero parece que solo encuentro los tipos de datos 'Int' y 'Entero'.

que podría utilizar la canónica

data Nat = Zero | Succ Nat 

pero luego no pude usar 1, 4, ... para denotar ellos.

Entonces pregunto, ¿hay alguna manera de lograr esto? (que es como usar 'unsigned' en C)

Gracias de antemano.

EDIT: voy el camino de ocultarlo dentro de un módulo, como se explica por C. A. McCann. Además, debo agregar el siguiente enlace: http://haskell.org/haskellwiki/Smart_constructors para obtener un resumen sobre el tema. ¡Gracias por tomarse el tiempo para responder!

Answer 1

lo general hay dos enfoques para esto: La definición inductiva que diste, o un tipo abstracto de datos utilizando algo más para la representación interna.

Tenga en cuenta que la representación inductiva no es terriblemente eficiente para números grandes; sin embargo, puede ser flojo, lo que le permite hacer cosas como ver cuál de dos nats es más grande sin evaluar más allá del tamaño del más pequeño.

Un tipo de datos abstracto es uno que se define en un módulo separado y no exporta sus constructores, por ejemplo IO o Data.Set.Set. Se puede definir algo como esto:

module Nat (Nat() {- etc. -}) where 

newtype Nat = Nat { unNat :: Integer } 

... donde se exporta varias operaciones en Nat de tal manera que, a pesar de que la representación internaes sólo Integer, se asegura de que ningún valor de tipo Nat se construye la celebración de una valor negativo.

En ambos casos, si desea utilizar literales numéricos, necesitará una definición de fromInteger, que se adjunta a la clase de tipo Num, lo cual es completamente incorrecto para los números naturales, pero bueno.

Si no le importa hacer una instancia roto sólo para obtener las sutilezas sintácticas, se puede hacer algo como esto:

instance Num Nat where 
    Zero + n = n 
    n + Zero = n 
    (Succ n1) + (Succ n2) = Succ . Succ $ n1 + n2 

    fromInteger 0 = Zero 
    fromInteger i | i > 0 = Succ . fromInteger $ i - 1 

... y así sucesivamente, para las otras funciones.El mismo se puede hacer para el enfoque de tipo abstracto de datos, pero tenga cuidado de no utilizar deriving para obtener una automática Num ejemplo, ya que estará feliz de romper su limitación no negativo.

Answer 2

Puede utilizar Word32 de Data.Word, que corresponde a uint32_t en C.

Con Word32 a obtener los mismos problemas que con los tipos sin signo de C, sobre todo exceso o por defecto. Si quiere asegurarse de que eso no suceda, deberá envolverlo en un nuevo tipo y solo exportar un constructor inteligente. Por lo tanto, no sería posible sumar, restar, etc., y no hay riesgo de exceso o defecto de flujo. Si desea admitir la adición, por ejemplo, puede agregar y exportar una función para agregar entradas sin firmar, pero con una verificación de desbordamiento (y con una penalización de rendimiento). A continuación, podría tener este aspecto:

module NT(UInt, addUInts) where 

import Data.Word 

newtype UInt = UInt Word32 
    deriving (Show) 

mkUInt :: Word32 -> UInt 
mkUInt = UInt 

addUInts :: UInt -> UInt -> Maybe UInt 
addUInts (UInt u1) (UInt u2) = 
    let u64 :: Word64 
     u64 = fromIntegral u1 + fromIntegral u2 
    in if u64 > fromIntegral (maxBound :: Word32) 
     then Nothing 
     else Just (UInt (fromIntegral u64)) 

Answer 3

No puedo recordar si se dirige a su pregunta específica, pero es posible que como el papel de Colin Runciman What about the natural numbers?. En caso de no poder superar el muro de pago, parece que hay un version at Citeseer.