C'è un modo per separare gli elenchi infiniti e finiti?

Question

Per esempio, sto scrivendo una funzione per le liste e voglio usare la funzione lunghezza

foo :: [a] -> Bool 
foo xs = length xs == 100 

Come può una persona comprendere questa funzione potrebbe essere utilizzata con liste infinite o no?

O devo sempre pensare a liste infinite e usare qualcosa di simile

foo :: [a] -> Bool 
foo xs = length (take 101 xs) == 100 

invece di usare direttamente la lunghezza?

E se Haskell avrebbe tipo FiniteList, quindi la lunghezza e foo sarebbe

length :: FiniteList a -> Int 
foo :: FiniteList a -> Bool 

Answer 1

length attraversa l'intero elenco, ma per determinare se una lista ha una particolare lunghezza n avete solo bisogno di guardare la prima n elementi.

L'idea di utilizzare take funzionerà. In alternativa si può scrivere una funzione lengthIs come questo:

-- assume n >= 0 
lengthIs 0 [] = True 
lengthIs 0 _ = False 
lengthIs n [] = False 
lengthIs n (x:xs) = lengthIs (n-1) xs 

È possibile utilizzare la stessa idea di scrivere le lengthIsAtLeast e lengthIsAtMost varianti.

Answer 2

In corso di modifica: sono in grado di rispondere in modo primitivo alla domanda nel titolo anziché alle specifiche del particolare esempio (per il quale la risposta di ErikR è eccellente).

Un gran numero di funzioni (come ad esempio length) sulle liste ha senso solo per gli elenchi finiti. Se la funzione che stai scrivendo ha senso solo per gli elenchi finiti, rendila chiara nella documentazione (se non è ovvia). Non esiste alcun modo per applicare la restrizione in quanto il problema di interruzione è irrisolvibile. Semplicemente non c'è algoritmo per determinare in anticipo se la comprensione

takeWhile f [1..] 

(dove f è un predicato su interi) produce un finito o una lista infinita oppure no.

Answer 3

ErikR e John Coleman hanno già risposto le parti principali della sua domanda, ma vorrei far notare qualcosa in più:

E 'meglio scrivere le funzioni in un modo che semplicemente non dipendono sulla finitezza o l'infinito dei loro input - a volte è impossibile ma molto spesso è solo una questione di riprogettazione. Ad esempio, invece di calcolare la media dell'intero elenco, è possibile calcolare una media corrente, che è di per sé una lista; e questa lista sarà di per sé infinita se la lista di input è infinita e finita altrimenti.

avg :: [Double] -> [Double] 
avg = drop 1 . scanl f 0.0 . zip [0..] 
    where f avg (n, i) = avg * (dbl n/dbl n') + 
         i   /dbl n'  where n' = n+1 
                 dbl = fromInteger 

nel qual caso si potrebbe mediare una lista infinita, di non dover prendere il suo length:

*Main> take 10 $ avg [1..] 
[1.0,1.5,2.0,2.5,3.0,3.5,4.0,4.5,5.0] 

---

In altre parole, una possibilità è quella di progettare il più delle vostre funzioni semplicemente non si preoccupa dell'aspetto infinito e ritarda la valutazione (completa) delle liste, e di altre strutture di dati (potenzialmente infiniti), fino a una fase più tardiva del programma.

In questo modo, immagino, saranno anche più riutilizzabili e componibili - qualsiasi cosa con presupposti meno o più generali sui suoi input, tende ad essere più componibile; viceversa, qualsiasi cosa con ipotesi più o più specifiche tende ad essere meno componibile e quindi meno riutilizzabile.

Answer 4

Nat s e pigrizia sciopero ancora:

import Data.List 

data Nat = S Nat | Z deriving (Eq) 

instance Num Nat where 
    fromInteger 0 = Z 
    fromInteger n = S (fromInteger (n - 1)) 

    Z + m = m 
    S n + m = S (n + m) 

lazyLength :: [a] -> Nat 
lazyLength = genericLength 

main = do 
    print $ lazyLength [1..] == 100 -- False 
    print $ lazyLength [1..100] == 100 -- True 

Answer 5

Ci sono un paio di modi diversi per fare un tipo di elenco finita. Il primo è semplicemente quello di fare le liste rigorosi nella loro spine:

data FList a = Nil | Cons a !(FList a) 

Purtroppo, questo butta via tutti i benefici di efficienza di pigrizia. Alcuni di questi possono essere recuperati utilizzando elenchi lunghezza indicizzata invece:

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE ScopedTypeVariables #-} 
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-} 

data Nat = Z | S Nat deriving (Show, Read, Eq, Ord) 

data Vec :: Nat -> * -> * where 
    Nil :: Vec 'Z a 
    Cons :: a -> Vec n a -> Vec ('S n) a 

instance Functor (Vec n) where 
    fmap _f Nil = Nil 
    fmap f (Cons x xs) = Cons (f x) (fmap f xs) 

data FList :: * -> * where 
    FList :: Vec n a -> FList a 

instance Functor FList where 
    fmap f (FList xs) = FList (fmap f xs) 

fcons :: a -> FList a -> FList a 
fcons x (FList xs) = FList (Cons x xs) 

funcons :: FList a -> Maybe (a, FList a) 
funcons (FList Nil) = Nothing 
funcons (FList (Cons x xs)) = Just (x, FList xs) 

-- Foldable and Traversable instances are straightforward 
-- as well, and in recent GHC versions, Foldable brings 
-- along a definition of length. 

GHC non consente tipi infinite, quindi non c'è modo per costruire un infinito Vec e quindi non c'è modo per costruire un infinito FList (1). Tuttavia, un FList può essere trasformato e consumato un po 'pigramente, con i benefici della cache e della garbage collection che ne derivano.

(1) Si noti che le forze di sistema di tipo fcons siano rigorosa nel suo argomento FList, così qualsiasi tentativo di fare un nodo con FList sarà il fondo.