superiore Kinded Tipi di Scala e Haskell

Question

Data.Foldable mostra il seguente tipo di dati algebrico:

data Tree a = Empty | Leaf a | Node (Tree a) a (Tree a)

sua kind è * -> *. Richiede un tipo a.

Prelude> :k Tree 
Tree :: * -> * 

Guardiamo ora al trait Foldable[_], un "tipo alto-kinded" da Scala da Functional Programming in Scala:

trait Foldable[F[_]] { 
    def foldRight[A,B](as: F[A])(z: B)(f: (A,B) => B): B 
    ... 
} 

L'eccellente libro dice:

Proprio come i valori e le funzioni hanno i tipi , tipi e costruttori di tipi hanno tipi. Scala usa tipi di monitorare il numero di argomenti tipo un costruttore di tipo prende, ...

EDIT

Quando si specifica trait Foldable[F[_]], fa il F[_] indicano sempre un tipo alto-kinded? È possibile che F[_] sia qualcos'altro? Potrebbe essere un tipo - F[A]?

Answer 1

Il F[_] a Scala sta per qualcosa come * -> * in Haskell: che è un tipo che "riceve" un tipo concreto (la _ in Scala e il primo * in Haskell) e restituisce un nuovo tipo di cemento (F[A] per un po 'di cemento digitare A e calcestruzzo "contenitore" F in Scala).

Quindi sì, F[_] corrisponde a un tipo di tipo superiore come List[_] o Option[_]. Non sarebbe utile definire traversabili in scala come trait Foldable[A,F[A]] perché dovremmo dire che Foldable deve essere definito con la cosa specifica che viene piegata (il A).

Answer 2

Non hai posto molte domande, ma se vuoi un'idea generale: sì, il sistema "gentile" di entrambe queste lingue è un sistema di tipi per il proprio sistema di tipi. Il tipo * non è un carattere jolly ma un atomo di tipo speciale; * è il tipo di "tipi di calcestruzzo" come String, [String] e Tree String.

A turno ci sono cose come [] o Tree (vedere la differenza?) Che hanno tipo * -> *; questo è il tipo di "tipi parametrizzati singolarmente" che prendono un tipo concreto e producono un altro tipo concreto.

Un ultimo esempio: ci sono cose chiamate "trasformatori monade" come MaybeT che prende una monade come IO e produce un altro monade come IO . Maybe (si perdoni l'uso di operatori di composizione delle funzioni dove non sono generalmente ammessi). Che tipo ha? Perché, (* -> *) -> * -> * ovviamente: le monadi hanno il tipo * -> *, quindi prendiamo uno di questi tipi e lo trasformiamo in un altro di questi tipi.

Non posso parlare con tanta esperienza in sintassi Scala, ma su internet si vede una definizione di un tratto trasformatori monade a Scala come:

trait MonadTrans[F[_[_], _]] { 
    def lift[G[_] : Monad, A](a: G[A]): F[G, A] 
} 

quindi penso che la tua ipotesi è per lo più a destra (che il parentesi indicano un tipo dipendente).

Avere una teoria dei tipi di queste cose garantisce di non scrivere mai cose come IO IO come tipo concreto o MaybeT String.

Answer 3

F[_]in questo contesto, ovvero come parametro di tipo per una classe o un metodo, indica sempre un tipo di tipo più elevato, ovvero un costruttore di tipi. Puoi anche scriverlo come F[A] ma normalmente lo farei solo se dovessi riutilizzare lo A per esprimere un vincolo, ad es. trait Something[F[A] <: Iterable[A]].

Come dice il libro, il tipo limita le cose (tipi o tipi di costruttori) che possono essere inserite lì. Puoi avere un Foldable[List] o un Foldable[Option], perché questi sono costruttori di tipo a 1 argomento, ma non puoi avere un Foldable[String] o un Foldable[Either]. Allo stesso modo non è possibile avere un Foldable[List[Int]], perché List[Int] è un tipo normale come String (ovvero di tipo *). E tu puoi avere un pieghevole per il tipo che è T[A] = Either[String, A], perché questo è un tipo a 1 parametro, alias un costruttore di tipo a 1 argomento, ovvero un tipo di tipo * -> *, anche se devi scriverlo usando la sintassi alquanto straziante Foldable[({type T[A]=Either[String, A]})#T]. E si può vedere che sarebbe solo possibile implementare il dato foldRight per "tipi" (costruttori di tipi) F che hanno la "forma" corretta; se F è Int, allora cosa sarebbe F[A] essere?

C'è un diverso utilizzo di scala di F[_] per indicare un tipo esistenziale, F[A] forSome { type A }; cerca di non confonderlo, non sono collegati.