Qual è lo scopo dei tipi di dati algebrici senza un costruttore?

Question

In Haskell si può definire un tipo di dati algebrico senza un costruttore:

data Henk 

Ma qual è lo scopo di un tipo (o genere?), Che non ha un costruttore?

Answer 1

Le macchine di tipo livello spesso richiedono tipi di esistere ma non costruiscono mai valori di tali tipi.

per esempio, i tipi di fantasma:

module Example (Unchecked, Checked, Stuff()) where 

data Unchecked 
data Checked 
data Stuff c = S Int String Double 

check :: Stuff Unchecked -> Maybe (Stuff Checked) 
check (S i s d) = if i>43 && ... 
        then Just (S i s d) 
        else Nothing 

readFile :: Filepath -> IO (Stuff Unchecked) 
readFile f = ... 

workWithChecked :: Stuff Checked -> Int -> String 
workWithChecked stuff i = ... 

workWithAny :: Stuff any -> Int -> Stuff any 
workWithAny stuff i = ... 

Finché il costruttore S non viene esportato dal modulo, l'utente di questa libreria non può forgiare lo stato "controllato" sul tipo di dati Stuff.

Sopra, la funzione workWithChecked non deve disinfettare l'input ogni volta che viene chiamato. L'utente deve averlo già fatto, dal momento che deve fornire un valore nel tipo "controllato" - e questo significa che l'utente ha dovuto chiamare in anticipo la funzione check. Questo è un design efficiente e robusto: non ripetiamo più volte lo stesso controllo ad ogni chiamata, e tuttavia non permettiamo all'utente di passare i dati non controllati.

Nota come i valori dei tipi Checked, Unchecked non sono rilevanti - non li usiamo mai.

Come altri menzionati nei commenti, ci sono molti altri usi dei tipi vuoti rispetto ai tipi fantasma. Ad esempio, alcuni GADT riguardano tipi vuoti. Per esempio.

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

Sopra utilizziamo tipi vuoti per registrare le informazioni sulla lunghezza nei tipi.

Inoltre, sono necessari i tipi senza costruttori per raggiungere alcune proprietà teorici: se cerchiamo un a tale che Either a T è isomorfo a T, vogliamo a essere vuoto. Nella teoria dei tipi, un tipo vuoto è comunemente usato come equivalente di tipo di una proposizione logicamente "falsa".