Tengo un ejercicio en el que tengo que definir un tipo para representar una lista con 0 a 5 valores. Primero pensé que podría resolver esto de forma recursiva así:

data List a = Nil | Content a (List a)

Pero no creo que este sea el enfoque correcto. ¿Puedes por favor darme un poco de pensamiento?

20
mayerph 29 abr. 2020 a las 16:19

3 respuestas

La mejor respuesta

No responderé su ejercicio por usted; para los ejercicios, es mejor averiguar la respuesta usted mismo, pero aquí hay una pista que lo llevará a la respuesta: puede definir una lista con 0 a 2 elementos como

data List a = None | One a | Two a a

Ahora, piense en cómo puede extender esto a cinco elementos.

11
bradrn 29 abr. 2020 a las 13:30

Bueno, una solución recursiva es ciertamente lo normal y de hecho agradable en Haskell, pero es un poco complicado limitar el número de elementos en ese momento. Entonces, para una solución simple al problema, primero considere la estúpida pero funcional dada por bradm.

Con la solución recursiva, el truco consiste en pasar una variable de "contador" por la recursividad y luego deshabilitar el consumo de más elementos cuando se alcanza el máximo permitido. Esto se puede hacer muy bien con un GADT:

{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeInType, StandaloneDeriving #-}

import Data.Kind
import GHC.TypeLits

infixr 5 :#
data ListMax :: Nat -> Type -> Type where
  Nil :: ListMax n a
  (:#) :: a -> ListMax n a -> ListMax (n+1) a

deriving instance (Show a) => Show (ListMax n a)

Entonces

*Main> 0:#1:#2:#Nil :: ListMax 5 Int
0 :# (1 :# (2 :# Nil))

*Main> 0:#1:#2:#3:#4:#5:#6:#Nil :: ListMax 5 Int

<interactive>:13:16: error:
    • Couldn't match type ‘1’ with ‘0’
      Expected type: ListMax 0 Int
        Actual type: ListMax (0 + 1) Int
    • In the second argument of ‘(:#)’, namely ‘5 :# 6 :# Nil’
      In the second argument of ‘(:#)’, namely ‘4 :# 5 :# 6 :# Nil’
      In the second argument of ‘(:#)’, namely ‘3 :# 4 :# 5 :# 6 :# Nil’
9
leftaroundabout 29 abr. 2020 a las 13:36

En aras de la exhaustividad, permítanme agregar un enfoque alternativo "feo", que sin embargo es bastante básico.

Recuerde que Maybe a es un tipo cuyos valores tienen la forma Nothing o Just x para algunos x :: a.

Por lo tanto, al reinterpretar los valores anteriores, podemos considerar Maybe a como un "tipo de lista restringida" donde las listas pueden tener cero o un elemento.

Ahora, (a, Maybe a) simplemente agrega un elemento más, por lo que es un "tipo de lista" donde las listas pueden tener uno ((x1, Nothing)) o dos ((x1, Just x2)) elementos.

Por lo tanto, Maybe (a, Maybe a) es un "tipo de lista" donde las listas pueden tener cero (Nothing), uno (Just (x1, Nothing)) o dos ((Just (x1, Just x2)) elementos.

Ahora debería poder entender cómo proceder. Permítanme enfatizar nuevamente que esta no es una solución conveniente de usar, pero es (IMO) un buen ejercicio para entenderlo de todos modos.


Usando algunas características avanzadas de Haskell, podemos generalizar lo anterior usando una familia de tipos:

type family List (n :: Nat) (a :: Type) :: Type where
    List 0 a = ()
    List n a = Maybe (a, List (n-1) a)
6
chi 30 abr. 2020 a las 07:40