Higher types in Scala and Haskell

Question

Data.Foldable shows the following type of algebraic data:

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

His kind - * -> * . This requires type a .

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

Now consider trait Foldable[_] , the “higher type” from Scala from Functional Programming in Scala :

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

A great book reads:

Just as values ​​and functions have types, types and type constructors have types. Scala uses views to track the number of arguments of type type. The constructor takes, ...

EDIT

When specifying trait Foldable[F[_]] , F[_] always indicates a higher type? Is it possible for F[_] be something else? Could it be type - F[A] ?

Answer 1

F[_] in Scala means something like * -> * in Haskell: it is a type that "gets" a particular type ( _ in Scala and the first * in Haskell) and returns a new specific type ( F[A] for a specific type A and the specific "container" F in Scala).

So yes, F[_] means a higher type of type List[_] or Option[_] . It would be impractical to define traversable in Scala as trait Foldable[A,F[A]] , because we will say that Foldable must be defined using a folding thing ( A ).

Answer 2

You did not ask a big question, but if you need a general idea: yes, the “prominent” system of both of these languages ​​is a type system for their own type system. Type * not a wildcard, but a special type of atom; * - the type of "specific types" such as String , [String] and Tree String .

In turn, there are such things as [] or Tree (see the difference?), Which have the form * -> * ; it is a type of "one-parameterized types" that take a particular type and produce another specific type.

Last example: there are things called “monad transformers,” such as MaybeT , which takes the monad as IO and creates another monad like IO . Maybe IO . Maybe (if you pardon the use of function composition operators, it is usually not allowed). What is it? Of course, (* -> *) -> * -> * , of course: monads have the form * -> * , so we take one of these types and convert it to the other of these types.

I cannot speak with much experience in Scala syntax, but on the Internet we see the definition of a monad transformer symbol in Scala as:

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

so I think your guess is basically correct (that the brackets point to the dependent type).

Having a type theory of these things ensures that you never write things like IO IO as a specific type, or MaybeT String .

Answer 3

F[_] in this context, that is, as a type parameter for a class or method, always means a type of a higher class that is a type constructor. You can also write it as F[A] , but usually you only do this if you intend to reuse A to express a constraint, for example. trait Something[F[A] <: Iterable[A]] .

As the book says, a view holds back what can be created there (types or type constructors). You can have Foldable[List] or Foldable[Option] because they are type constructors with 1 argument, but you cannot have Foldable[String] or Foldable[Either] . Likewise, you cannot have Foldable[List[Int]] , because List[Int] is a regular type of type String (that is, View * ). And you can have a folding one for type T[A] = Either[String, A] , because it is a type with 1 parameter, the so-called constructor of type 1 of the argument, also known as a type of type * -> * , although you need to write it, using the somewhat torturous syntax Foldable[({type T[A]=Either[String, A]})#T] . And you can see that it would be possible to implement this foldRight for the “types” (type constructors) of F that have the correct “shape”; if F is Int , then what would be F[A] ?

There is another use of scala F[_] to denote the existential type F[A] forSome { type A } ; try not to get confused in this, they are not released.