We assume that you are familiar with what we are doing without GADT. Say, for the simplest case, we are defining a list\uff1a<\/p>\n
List a = Nil | Cons a (List a)<\/pre>\nWhat exactly are we doing?<\/p>\n
List<\/code>. It takes a type as parameter, and returns a new type. It’s essentially a function of types<\/em>.<\/li>\n- On the RHS, it tells us that we have two ways to construct a value of type
List a<\/code>. One is called Nil<\/code>\u00a0and the other Cons a (List a)<\/code>.\n\n- You can directly write
Nil<\/code>\u00a0to get a value of type List a<\/code>, with type a<\/code>\u00a0to be determined, more precisely inferred from the context.<\/li>\n- In the case of
Cons a (List a)<\/code>, it’s actually a function named Cons<\/code>, taking two parameters, one with type a<\/code>, the other with type List a<\/code>. Again, the type of a<\/code>\u00a0should be inferred from the context. But this time it’s often more direct, as a<\/code>\u00a0is the type of the first parameter.<\/li>\n<\/ul>\n<\/li>\n<\/ul>\nThen we can represent these two constructors as normal functions:<\/p>\n
Nil :: List a\r\nCons :: a -> List a -> List a<\/pre>\nWe can see that they are functions both with the same return type List a<\/code>. The only thing that GADT does<\/em>, is allowing a specific a<\/code>\u00a0here. For example, we can have a constructor with a<\/code>\u00a0specifically set to Int<\/code>, meaning it only constructs values of type List Int<\/code>.<\/p>\nIntNil :: List Int<\/pre>\nWe can experiment with some code in the GADT flavor:<\/p>\n
data List a where\r\n IntNil :: List Int\r\n Nil :: List a\r\n Cons :: a -> List a -> List a\r\n\r\na :: List Int\r\na = IntNil\r\n\r\n-- Would raise an error for type incompatibility.\r\n-- c_ :: List Char\r\n-- c_ = IntNil\r\n\r\n-- This one is compatible.\r\nc :: List Char\r\nc = Nil<\/pre>\nCertainly, a<\/code>\u00a0does not have to be a type as simple as Int<\/code>. It could be an arbitrary type, even List a<\/code>\u00a0or List (List a)<\/code>\u00a0with a<\/code>\u00a0still unspecified:<\/p>\ndata Pair a b where Pair :: a -> b -> Pair a b\r\n\r\ndata List a where IntListNil :: List (List Int)\r\n ListNil :: List (List a)\r\n IntNil :: List Int\r\n Nil :: List a\r\n Cons :: a -> List a -> List a\r\n -- This one is invalid, since the top-level `Pair` is not `List`\r\n -- Bad :: a -> List a -> Pair a (List a)<\/pre>\nSo what can GADT be used for? What can be additionally done with it? Here are some scenarios as far as I know:<\/p>\n
The most famous use case is to embed (the AST of) a language into Haskell. Suppose we have such a simple language of expressions:<\/p>\n
data Expr = \r\n ILit Int\r\n | BLit Bool\r\n | Add Expr Expr\r\n | Eq Expr Expr<\/pre>\nSuch a data type definition is sufficient to contain the language, but it also contains expressions beyond the language (that is, invalid expressions). For example, Bool<\/code>\u00a0values cannot be Add<\/code>ed. But this definition does not prevents us from writing:<\/p>\naddBool :: Expr\r\naddBool = Add (BLit True) (BLit False)<\/pre>\nAn attempt to fix this is to record the “return type” of an Expr<\/code>\u00a0somewhere. Remember we have done that with List a<\/code>, where we record the member type a<\/code>\u00a0in the list type List a<\/code>. We can do the same to Expr<\/code>:<\/p>\ndata Expr a = \r\n ILit Int\r\n | BLit Bool\r\n | Add (Expr Int) (Expr Int)\r\n | Eq (Expr a) (Expr a)<\/pre>\nThis looks plausible. But there are still problems!<\/p>\n
The crucial part is, while\u00a0BLit True<\/code>\u00a0should be Expr Bool<\/code>\u00a0so that it cannot be the parameters of Add<\/code>, it isn’t actually. The BLit True<\/code>\u00a0here is still of type Expr a<\/code>\u00a0with a<\/code>\u00a0undetermined (to be inferred). This is parallel to the case where Nil<\/code>\u00a0is of type List a<\/code>\u00a0with a<\/code>\u00a0undetermined. There is actually no relation between the type of the parameter of the constructor BLit<\/code>\u00a0and the type of the constructed value.<\/p>\nHere GADT comes into the play. We can constraint the return type of the constructor only with GADT:<\/p>\n
data Expr a where\r\n ILit :: Int -> Expr Int\r\n BLit :: Bool -> Expr Bool\r\n Add :: Expr Int -> Expr Int -> Expr Int\r\n -- In the case of Eq, we can loosen the type specification into a typeclass.\r\n Eq :: Eq a => Expr a -> Expr a -> Expr Bool<\/pre>\nThis would achieve the goal:<\/p>\n
-- Won't compile, since `BLit True` and `BLit False` are of type `Expr Bool`\r\n-- addBool = Add (BLit True) (BLit False)\r\naddInt = Add (ILit 1) (ILit 2)\r\neqBool = Eq (BLit True) (BLit False)<\/pre>\nFantastic!<\/p>\n
This is the so-called “initial embedding” of a language. The final version we achieved with GADT is a “tagless\u00a0 initial embedding”. Why tagless? Because ADT is the so-called “tagged union”, and we are abandoning it, thus tagless.<\/p>\n
The Expr<\/code>\u00a0represents a very simple language. You can well embed more complex languages such as simply type lambda calculus.<\/p>\nContrary to “initial embedding”, there’s “final embedding” as well. But that’s another story.<\/p>\n
\nWe can even impose more restrictions on the embed of languages. Suppose we have a language describing stack operations. Push<\/code>\u00a0means push a number to the top of the stack. Add<\/code>\u00a0means pop the top two numbers and push back their sum:<\/p>\ndata StackLang where\r\n Begin :: StackLang\r\n Push :: Int -> StackLang -> StackLang\r\n Add :: StackLang -> StackLang\r\n\r\nbug = Add (Push 1 Begin)<\/pre>\nThe bug<\/code>\u00a0line reflects a bug that would happen. When there’s only one element in the stack, an Add<\/code>\u00a0could not be performed. If only we could eliminate such silly bugs on the type level!<\/p>\nThis could be possible when the number of elements in the stack is encoded in the type StackLang<\/code>. This is exactly where GADT shines:<\/p>\ndata Z\r\ndata S n\r\n\r\ndata SStackLang t where\r\n SBegin :: SStackLang Z\r\n SPush :: Int -> SStackLang t -> SStackLang (S t)\r\n SAdd :: SStackLang (S (S t)) -> SStackLang (S t)<\/pre>\nThe Z<\/code>\u00a0(for 0) and S<\/code>\u00a0(for successor<\/em>) here are simulations of the Peano system of natural numbers. Now compiling the following<\/p>\nsBug = SAdd (SPush 1 SBegin)<\/pre>\nwould raise an error:<\/p>\n
\u2022 Couldn\u2019t match type \u2018Z\u2019 with \u2018S t\u2019
\nExpected type: SStackLang (S (S t))
\nActual type: SStackLang (S Z)<\/p><\/blockquote>\n
Safe as expected.<\/p>\n
This is actually a simulation of the dependent type<\/em>. You can define types representing “lists of length n” and so on in this way.<\/p>\nGADT can also convert types into values. You can do this without GADT:<\/p>\n
data Witness a = Witness a<\/pre>\nBut you need to supply a value of type a<\/code>.\u00a0 What if you cannot find such a value? It’s not reasonable to require a value to encode a type, as such a value may not exist at all! (consider Void<\/code>)<\/p>\nYou can drop this requirement with GADT:<\/p>\n
data Witness a where\r\n IntWitness :: Witness Int\r\n BoollWitness :: Witness Bool<\/pre>\nIn this way, you directly get a value in the encoded type Witness a<\/code>, even if there’s no value of the original type a<\/code>.<\/p>\nThis is the so called “type witness”. But how can this be used? (to be continued)<\/p>","protected":false},"excerpt":{"rendered":"
Sorry, this entry is only available in \u4e2d\u6587. For the sake of viewer convenience, the content is shown below in the alternative language. You may click the link to switch the active language.\u5148\u770b\u770b\u6ca1\u6709 GADT \u7684\u65f6\u5019\u6211\u4eec\u5728\u505a\u5565\u3002\u6700\u7b80\u5355\u7684\uff0c\u6bd4\u5982\u5b9a\u4e49\u4e00\u4e2a\u5217\u8868\uff1a List a = Nil | Cons a (List a) \u5b83\u662f\u5728\u505a\u5565\u5462\uff1f \u5148\u770b\u7b49\u53f7\u5de6\u8fb9\uff0c\u5b83\u9996\u5148\u5b9a\u4e49\u4e86\u4e00\u4e2a\u53eb List \u7684 type constructor\uff0c\u5b83\u63a5\u53d7\u4e00\u4e2a\u7c7b\u578b\uff0c\u5e76\u8fd4\u56de\u4e00\u4e2a\u65b0\u7684\u7c7b\u578b\u3002\u5176\u5b9e\u5c31\u662f\u7c7b\u578b\u7684\u51fd\u6570\u3002 \u518d\u770b\u53f3\u8fb9\uff0c\u5b83\u544a\u8bc9\u6211\u4eec\u6709\u4e24\u79cd\u65b9\u5f0f\u83b7\u5f97\u4e00\u4e2a\u7c7b\u578b\u4e3a List a \u7684\u503c\uff0c\u4e00\u4e2a\u53eb Nil\uff0c\u4e00\u4e2a\u53eb … Continue reading “What is GADT (Generalized Algebraic Data Types) in Haskell?”<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":[],"categories":[16],"tags":[34,32],"_links":{"self":[{"href":"https:\/\/colliot.org\/en\/wp-json\/wp\/v2\/posts\/395"}],"collection":[{"href":"https:\/\/colliot.org\/en\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/colliot.org\/en\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/colliot.org\/en\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/colliot.org\/en\/wp-json\/wp\/v2\/comments?post=395"}],"version-history":[{"count":5,"href":"https:\/\/colliot.org\/en\/wp-json\/wp\/v2\/posts\/395\/revisions"}],"predecessor-version":[{"id":435,"href":"https:\/\/colliot.org\/en\/wp-json\/wp\/v2\/posts\/395\/revisions\/435"}],"wp:attachment":[{"href":"https:\/\/colliot.org\/en\/wp-json\/wp\/v2\/media?parent=395"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/colliot.org\/en\/wp-json\/wp\/v2\/categories?post=395"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/colliot.org\/en\/wp-json\/wp\/v2\/tags?post=395"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}