ГАДТ - приложения и полезность?

Question

Я рассказываю о GADT, используя learnyouahaskell, и меня интересует их возможное использование. Я понимаю, что их основной характеристикой является возможность явной установки типа.

Такие как:

data Users a where 
  GetUserName :: Int -> Users String
  GetUserId :: String -> Users Int

usersFunction :: Users a -> a 
usersFunction (GetUserName id) 
   | id == 100      = "Bob"
   | id == 200      = "Phil"
   | otherwise      = "No corresponding user"
usersFunction (GetUserId name)
   | name == "Bob"      = 100
   | name == "Phil"     = 200
   | otherwise          = 0

main = do
   print $ usersFunction (GetUserName 100)

Помимо добавления дополнительной безопасности типов при работе с этими типами данных, каковы другие применения GADT?

Answer 1

Glambda

Ричард Айзенберг делает очень убедительные аргументы в пользу ГАДЦ в glambda просто типизированный интерпретатор лямбда-исчисления, который использует GADT, чтобы убедиться, что плохо напечатанные программы просто не могут быть созданы. У Фила Вадлера есть нечто подобное и более простое, из которого был взят следующий образец

data Exp e a where
  Con :: Int -> Exp e Int
  Add :: Exp e Int -> Exp e Int -> Exp e Int
  Var :: Var e a -> Exp e a
  Abs :: Typ a -> Exp (e,a) b -> Exp e (a -> b)
  App :: Exp e (a -> b) -> Exp e a -> Exp e b

Идея состоит в том, что тип выражения (в интерпретаторе) кодируется в типе выражения, представленного в программе на Haskell.

Векторы, набранные в соответствии с их длиной

Используя GADT, мы можем добавить фантомный тип, который говорит нам, что мы отслеживаем длину вектора, который у нас есть. Этот пакет имеет хорошую реализацию. Это может быть переопределено несколькими способами (например, используя GHC.TypeLits натуральные числа уровня типа). Интересный тип данных (скопированный из источника связанного пакета)

data Vector (a :: *) (n :: Nat)  where
  Nil  :: Vector a Z
  (:-) :: a -> Vector a n -> Vector a (S n)

Тогда я могу написать безопасную версию head' :: Vector a (S n) -> a,

Ограничения

У меня нет хорошего примера, демонстрирующего полезность этого, но вы можете привязать ограничения к отдельным конструкторам в GADT. Ограничения, которые вы добавляете к конструкторам, применяются при создании чего-либо и доступны при сопоставлении с шаблоном. Это позволяет нам делать разные забавные вещи.

data MyGADT b where
  SomeShowable :: Show a => a -> b -> MyGADT b     -- existential types!
  AMonad :: Monad b => b -> MyGADT b