Type Constructor và Kind: Nền tảng để hiểu Higher-Kinded Types

Author: hoc081098Estimated 5 min readHits
Series: Type Constructor, Higher-Kinded Types và Type ClassesPart 1 of 1
kotlinhaskellfunctional-programmingtype-systemtype-constructorhigher-kinded-types

Chém gió nhiều về Functional Programming nhưng mình đôi lúc vẫn nhầm lẫn giữa Type Constructor, Higher-Kinded Types (HKT) và Type Classes. Đây là phần đầu của chuỗi note này, tập trung vào Type Constructor và Kind — nền tảng để đi tiếp tới Higher-Kinded Types và Type Classes.

💠 Type là thứ quá quen thuộc trong các ngôn ngữ lập trình như Kotlin, Dart, Java, v.v.

Ta thường xuyên gặp: Int, Long, Float, Double, Boolean/bool/Bool (tùy ngôn ngữ), String, List/Array, Set/Map, Function, ... Simple, right? Các type hoàn chỉnh như: Int, Long, Float, Double, Boolean, String, List<Int>, Map<String, Int>, Either<String, Int> có thể được dùng trực tiếp làm type của một value. Ví dụ với Kotlin:

val number: Int = 42
val integers: List<Int> = listOf(1, 2, 3)

Int là một type hoàn chỉnh. List<Int> cũng là một type hoàn chỉnh. Either<String, Int> cũng vậy.

💠 Tiếp đến là Type Constructor.

Nghe chữ constructor thì rất dễ liên tưởng tới class constructor. Class constructor được dùng để tạo ra một instance/value của class, chẳng hạn val user = User(...). Ở đây, class constructor hoạt động ở value-level.

Còn Type Constructor hoạt động ở một level khác. Ta có thể hình dung nó giống như một “function ở type-level”, nhận vào một hoặc nhiều type và tạo ra một type mới. Ví dụ: List, Option, Either là các Type Constructor.

Để biểu diễn trực quan vị trí type argument còn thiếu, trong bài này ta dùng pseudonotation List<_>, Option<_>, Either<L, _>, ... Lưu ý rằng đây không phải là cú pháp của Kotlin, Haskell hay Scala. Các biểu thức List<_>, ... trên chưa phải là các type hoàn chỉnh vì vẫn còn thiếu type argument, trong đó _ chỉ đóng vai trò placeholder. Khi ta cung cấp type nào đó để điền vào chỗ trống _, ta mới thu được một type hoàn chỉnh.

Ví dụ: List<_> có thể hình dung tương đương với một hàm nhận một type A và trả về type List<A>. Ta có thể mô tả mapping này bằng notation trung lập A ↦ List<A>. Tương tự với Either, vì Either có 2 type argument, nên khi ta cố định 1 type argument L, thì ta thu được một Type Constructor Either<L, _>, và Type Constructor này nhận 1 type argument R và trả về type hoàn chỉnh Either<L, R>. Mapping tương ứng là R ↦ Either<L, R>.

Ta có thể hiểu trực giác rằng Type Constructor giống một function nhận type và tạo ra type. Lưu ý rằng đây chỉ là một cách hình dung để dễ hiểu. Type Constructor không phải runtime function theo nghĩa thông thường, mà là một cấu trúc ở type-level.

💠 Kind

Đến đây xuất hiện thêm một khái niệm nữa, đó là Kind.

Nếu type mô tả một value 42 :: Int, ta hiểu rằng value 42 có type Int. Vậy ta có câu hỏi tương tự ở type-level: “type Int thuộc Kind nào?” Hay nói dân dã, thì “Type của type Int là gì?”

Với Haskell, Int là một type hoàn chỉnh và có Kind là Type. Ta viết là Int :: Type. Trong GHC, * là legacy notation cho Type, nhưng Type mới là cách viết được khuyến nghị hiện nay.

Có thể nhớ mối quan hệ rất đơn giản:

value : type
type  : kind

Ví dụ:

42  : Int
Int : Type

💠 Tiếp tục với Type Constructor

Một type constructor như List chưa phải type hoàn chỉnh vì nó vẫn cần thêm một type argument. Conceptually, List :: Type -> Type có nghĩa là List nhận một Type và trả về một Type. Khi ta truyền vào một type argument, ví dụ Int, ta thu được một type hoàn chỉnh là List<Int>. Và khi đó List<Int> :: Type.

Tương tự với Either: Either :: Type -> Type -> Type Nó cần hai type argument. Sau khi truyền argument đầu tiên, ví dụ String, ta được Either<String, _> :: Type -> Type. Sau khi truyền tiếp argument thứ hai, ví dụ Int, ta thu được một type hoàn chỉnh Either<String, Int> :: Type.

Các kind judgments tương ứng, theo notation hiện đại của Haskell/GHC:

Either            :: Type -> Type -> Type
Either String     :: Type -> Type
Either String Int :: Type

Đây là điểm Haskell thể hiện những khái niệm này rất rõ. Haskell có thể phân biệt: Int :: Type là một type hoàn chỉnh trong khi một type constructor có một tham số có dạng Type -> Type, và type constructor hai tham số có dạng Type -> Type -> Type.

💠 Có thể tóm gọn bằng mấy dòng này:

// value : type
42          : Int

// type : kind
Int         : Type
List<Int>   : Type
Either<L,R> : Type

// type constructor
List        : Type -> Type
List<Int>   : Type

// type constructor
Either      : Type -> Type -> Type
Either<L,_> : Type -> Type
Either<L,R> : Type

Đến đây ta mới bắt đầu có nền tảng để nói tiếp về Higher-Kinded Types:

Nói theo mental model về Kind ở phần trên, Generic type parameter thông thường trong các ngôn ngữ lập trình như Java, Kotlin, Dart và C# chỉ đại diện cho những type có Kind Type (còn gọi là proper types), chứ không thể đại diện cho Kind “cao hơn” được.

Ví dụ với Kotlin:

interface Monoid<T> {
    fun empty(): T
    fun combine(a: T, b: T): T
}

T ở đây chỉ có thể là các type đầy đủ như Int, Long, List<Int>, List<Long> hoặc Either<String, Int>. T không thể đại diện cho List<_>, Either<L, _> hay Either<_, _> được.

Vì vậy, các ngôn ngữ này không cho phép ta trực tiếp abstract trên các Type Constructor có Kind cao hơn Type.

Còn HKT, ở những ngôn ngữ hỗ trợ nó như Haskell, Scala và Flix, lại cho phép ta abstract trên chính những Type Constructor có Kind cao hơn như vậy. Nhưng cái đó để phần sau 😄.