notes

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Try.GADT.GADT where

GADTs

• Wikibooks (src):

  With GADTs, a constructor for Foo a is not obliged to return Foo a; it can return any Foo blah that you can think of.

  data TrueGadtFoo a where
    MkTrueGadtFoo :: a -> TrueGadtFoo Int
  

  • Still, need to use a relevant data constructor

    data Foo where
      MkFoo :: Bar Int -- This will not typecheck
    

• Support record syntax - src

  • example

• Is it considered a good practice to put constraints in consructors inside GADT declaration?

  • No. Use a compiler to derive instances like Functor, put constraints in functions.

Heterogeneous list

src

data HList_ xs where
  HNil_ :: HList_ '[]
  (:::) :: a -> HList_ as -> HList_ (a ': as)

infixr 6 :::

hex :: HList_ '[Char, Integer, String]
hex = 'a' ::: 1 ::: "hello" ::: HNil_

Non-empty list

data Empty
data NonEmpty

data SafeList a b where
  Nil :: SafeList a Empty
  Cons :: a -> SafeList a b -> SafeList a NonEmpty

safeHead :: SafeList a NonEmpty -> a
safeHead (Cons a _) = a

safeTail :: SafeList a b -> a
safeTail (Cons a Nil) = a
safeTail (Cons _ b) = safeTail b

st1 :: Integer
st1 = safeTail $ Cons 3 (Cons 4 Nil)

-- >>>st1
-- 4