Haskell #13: Dạng

Dạng

Type constructor nhận vào tham số là kiểu rồi tạo ra kiểu cụ thể. Điều này làm tôi nhớ đến hàm, chúng nhận vào tham số là giá trị để tạo ra giá trị. Ta đã thấy type constructor có thể áp dụng từng phần (Either String) là một kiểu, nó nhận vào một kiểu và tạo ra kiểu cụ thể, như Either String Int), giống như hàm.

Trong mục này, ta sẽ định nghĩa cách áp dụng kiểu cho type constructor, cũng như xét định nghĩa áp dụng hàm bằng khai báo kiểu. Phần này không bắt buộc, tuy nhiên nắm được vấn đề này sẽ cho bạn hiểu biết tường tận về hệ thống kiểu của Haskell hơn.

Những giá trị như 3, “YEAH” hoặc takeWhile (các hàm cũng là giá trị, vì ta có thể dùng chúng dưới dạng tham số) mỗi cái đều có kiểu riêng. Kiểu đơn giản là nhãn mà mỗi giá trị mang theo để dựa vào đó ta có thể suy luận về giá trị của chúng. Nhưng bản thân kiểu lại còn có nhãn của riêng chúng, gọi là dạng (kind). Dạng thì ít nhiều giống kiểu của kiểu. Điều này nghe hơi kì quặc và dễ gây nhầm lẫn, song thực ra đó là một khái niệm rất hay.

Dạng là gì và chúng dùng được vào việc gì? À, ta hãy xét dạng của một kiểu bằng cách dùng lệnh :k trong GHCI.

ghci> :k Int
Int :: *

Dấu * dùng để ám chỉ một kiểu cụ thể nào đó. Một kiểu cụ thể là kiểu không nhận bất kì tham số kiểu nào (xin nhắc lại, giá trị bất kì chỉ nằm trong kiểu cụ thể). Hãy thử nghiệm với Maybe là gì.

ghci> :k Maybe
Maybe :: * -> *

Type constructor Maybe nhận vào kiểu cụ thể (chẳng hạn, Int) rồi trả về kiểu cụ thể, chẳng hạn Maybe Int. Và đó chính là điều mà dạng cho ta biết. Cũng như Int -> Int là hàm nhận vào Int và trả về Int, * -> * trừu tượng hơn, có nghĩa là type constructor nhận vào và trả về một kiểu cụ thể (có thể là String, Char, …). Sau khi áp dụng tham số kiểu cho Maybe:

ghci> :k Maybe Int
Maybe Int :: *

Chúng ta thu về kiểu cụ thể (đó là điều mà * -> * muốn nói). Một cách so sánh (mặc dù không tương đương, vì kiểu và dạng là khác nhau) là giữa hai đối tượng isUpper và isUpper 'A'. isUpper có kiểu là Char -> Bool và isUpper 'A' có kiểu là Bool. Tuy vậy cả hai kiểu trên đều có dạng là *.

Một dạng khác:

ghci> :k Either
Either :: * -> * -> *

Thông tin này cho ta biết Either nhận vào hai kiểu cụ thể và tạo ra một kiểu cụ thể mới. Nó cũng như khai báo một hàm nhận vào hai giá trị và trả về một thứ gì đó. Type constructor được curry (cũng giống với hàm), vì vậy ta có thể áp dụng từng phần.

ghci> :k Either String
Either String :: * -> *
ghci> :k Either String Int
Either String Int :: *

Khi ta muốn làm cho Either thuộc về functor, ta phải áp dụng từng phần vì Functor muốn kiểu chỉ nhận một tham số trong khi Either thì nhận hai. Nói cách khác, Functor nhận kiểu có dạng là * -> * và vì vậy ta phải áp dụng Either từng phần để thu được kiểu có dạng * -> * thay vì kiểu ban đầu của nó, * -> * -> *. Nếu ta nhìn vào định nghĩa của Functor lần nữa:

class Functor f where 
    fmap :: (a -> b) -> f a -> f b

có thể thấy rằng f có vai trò nhận vào kiểu cụ thể và tạo ra kiểu cụ thể. Ta biết nó phải tạo ra kiểu cụ thể vì nó chính là giá trị được sử dụng trong a -> b. Và từ đó, ta có thể suy diễn rằng những kiểu muốn kế thừa Functor phải có dạng * -> *.

Bây giờ, tôi tạo ra một kiểu linh tinh:

class Tofu t where
    tofu :: j a -> t a j

Trước hết hãy tìm hiểu dạng của nó. Bởi j a được dùng làm kiểu của một giá trị mà hàm tofu nhận vào làm tham số, nên j a phải có dạng là *. Ta giả sử a có dạng *, suy ra j phải có dạng * -> *. Ta thấy rằng t cũng phải tạo ra giá trị cụ thể và nó phải nhận hai kiểu. Đồng thời biết rằng a có dạng * và j có dạng * -> *, suy ra t phải có dạng * -> (* -> *) -> *. Cuối cùng, t nhận một kiểu cụ thể a, một type constructor j nhận vào một kiểu cụ thể rồi tạo ra một kiểu cụ thể mới.

Sau đây là một cách để tạo một kiểu có dạng là * -> (* -> *) -> * (kiểu khai báo record).

data Frank a b  = Frank {
    frankField :: b a
} deriving (Show)

Trường frankField được khai báo để giữ giá trị, chúng phải có dạng *. Như vậy b a phải trả về kiểu có dạng *. Với trường hợp đơn giản nhất, ta giả sử a có dạng *, b phải nhận vào một tham số kiểu và dạng của b là * -> *. Bởi vì a và b là tham số kiểu cho Frank, dễ suy rằng Frank có dạng * -> (* -> *) -> *. Dấu * thứ nhất biểu diễn cho a, (* -> *) biểu diễn cho b.

ghci> :t Frank {frankField = Just "HAHA"}
Frank {frankField = Just "HAHA"} :: Frank [Char] Maybe
ghci> :t Frank {frankField = Node 'a' EmptyTree EmptyTree}
Frank {frankField = Node 'a' EmptyTree EmptyTree} :: Frank Char Tree
ghci> :t Frank {frankField = "YES"}
Frank {frankField = "YES"} :: Frank Char []

Bởi vì frankField có kiểu b a, nên những giá trị của nó phải có kiểu cũng với hình thức tương tự. Vì vậy chúng có thể là Just "HAHA" (Maybe [Char]) hoặc ['Y','E','S'] ([Char]).

Để Frank kế thừa Tofu là rất đơn giản. Dễ thấy rằng Tofu nhận vào j a (ví dụ Maybe Int) rồi trả về t a j. Vì vậy nếu ta thay thế Frank bằng j, kiểu của kết quả sẽ là Frank Int Maybe.

instance Tofu Frank where
    tofu x = Frank x
ghci> tofu (Just 'a') :: Frank Char Maybe
Frank {frankField = Just 'a'}
ghci> tofu ["HELLO"] :: Frank [Char] []
Frank {frankField = ["HELLO"]}

Một ví dụ khác:

data Barry t k p = Barry { 
    fp :: p, 
    sp :: t k 
} deriving (Show)

Giả sử ta muốn Barry kế thừa Functor. Functor cần kiểu dạng * -> * nhưng dường như Barry không có dạng này. Barry nhận vào ba tham số kiểu, vì vậy nó sẽ là something -> something -> something -> *. Đầu tiên trường fp có kiểu p, suy ra p có dạng là *. Đối với t và k, giống như ví dụ trước ta giả định là k có dạng * và t có dạng * -> *. Bây giờ hãy thay thế vào chỗ something, ta thu được dạng của Barry là:

ghci> :k Barry
Barry :: (* -> *) -> * -> * -> *

Để khiến Barry kế thừa Functor, ta phải áp dụng từng phần hai tham số đầu để còn lại * -> *. Điều đó có nghĩa rằng chỗ bắt đầu khai báo thể hiện sẽ là: instance Functor (Barry a b) where. Nếu ta fmap cho Barry, thì nó sẽ có kiểu fmap :: (a -> b) -> Barry c d a -> Barry c d b, vì ta chỉ thay thế f của Functor bằng Barry c d. Tham số kiểu thứ ba của Barry sẽ phải thay đổi và ta thấy rằng nó thuận tiện như ở nhà.

instance Functor (Barry a b) where
    fmap f (Barry {fp = x, sp = y}) = Barry {fp = f x, sp = y}

ghci> fmap (+2) (Barry {fp = 4 :: Int, sp = Just 4 :: Maybe Int})
ghci> Barry {fp = 6, sp = Just 4}

Tóm tắt lại, ta đã xét đến cách hoạt động của tham số kiểu và phần nào đã giải thích về mặt hình thức khái niệm “dạng”, giống như việc hình thức hóa tham số hàm với các khai báo hàm (cần lưu ý rằng chúng là hai thứ hoàn toàn khác nhau). Thực tế, khi làm việc với Haskell, bạn chẳng cần bận tâm với kiểu và suy diễn kiểu một cách thủ công như ta đã làm. Thông thường, bạn chỉ cần áp dụng từng phần kiểu dữ liệu của bạn cho * -> * hoặc * khi nó thành thể hiện của một trong các typeclass chuẩn; nhưng biết được nguyên nhân và cách thức hoạt động như vậy là một điều hay. Cũng thú vị khi thấy rằng bản thân kiểu lại có khái niệm cấu thành nhỏ hơn.

Kết thúc bài 13

Haskell #14: Applicative