Haskellにおける型レベルプログラミングの基本(翻訳) ref: https://qiita.com/HirotoShioi/items/39fc492401e4dcbc8cba

file0.txt

data Unit = MkUnit
data Bool = True | False

file1.txt

data IntAndChar = MkIntAndChar Int Char

file10.txt

data HigherKinded f a
    = Bare a
    | Wrapped (f a)

file11.txt

λ> :kind HigherKinded
HigherKinded :: (* -> *) -> * -> *

file12.txt

λ> data Void
λ> :kind Void
Void :: *

file13.txt

data Zero
data Succ a

type One = Succ Zero
type Two = Succ One
type Three = Succ Two
type Four = Succ (Succ (Succ (Succ Zero)))

file14.txt

{-# LANGUAGE DataKinds #-}

file15.txt

data Nat = Zero | Succ Nat

file16.txt

λ> :kind 'Zero
'Zero :: Nat
λ> :kind 'Succ
'Succ :: Nat -> Nat

file17.txt

λ> :type Zero
Zero :: Nat
λ> :type Succ
Succ :: Nat -> Nat

file18.txt

{-# LANGUAGE GADTs #-}

file19.txt

data Maybe a where
    Just :: a -> Maybe a
    Nothing :: Maybe a

file2.txt

theFirstOne = MkIntAndChar 3 'a'
theSecond   = MkIntAndChar (-3) 'b'

file20.txt

data IntBool a where
    Int :: Int -> IntBool Int
    Bool :: Bool -> IntBool Bool

file21.txt

extractIntBool :: IntBool a -> a
extractIntBool (Int _)  = 0
extractIntBool (Bool b) = b

file22.txt

data Vector (n :: Nat) a where

file23.txt

{-# LANGUAGE KindSignatures #-}

file24.txt

VNil :: Vector 'Zero a

file25.txt

VCons :: a -> Vector n a -> Vector ('Succ n) a

file26.txt

data Vector (n :: Nat) (a :: *) where
    VNil :: Vector 'Zero a
    VCons :: a -> Vector n a -> Vector ('Succ n) a

file27.txt

data Vector n a where
    VNil :: Vector Zero a
    VCons :: a -> Vector n a -> Vector (Succ n) a

file28.txt

instance Show a => Show (Vector n a) where
    show VNil         = "VNil"
    show (VCons a as) = "VCons " ++ show a ++ " (" ++ show as ++ ")"

file29.txt

{-# LANGUAGE TypeFamilies #-}

file3.txt

λ> :t MkIntAndChar
MkIntAndChar :: Int -> Char -> IntAndChar

file30.txt

add :: Nat -> Nat -> Nat

file31.txt

add Zero n = n

file32.txt

add (Succ n) m = add n (Succ m)

file33.txt

add :: Nat -> Nat -> Nat
add Zero n     = n
add (Succ n) m = add n (Succ m)

file34.txt

type family Add n m where

file35.txt

Add 'Zero n = n

file36.txt

Add ('Succ n) m = Add n ('Succ m)

file37.txt

    • The type family application ‘Add n ('Succ m)’
        is no smaller than the instance head
      (Use UndecidableInstances to permit this)
    • In the equations for closed type family ‘Add’
      In the type family declaration for ‘Add’

file38.txt

{-# LANGUAGE UndecidableInstances #-}

file39.txt

λ> :kind Add (Succ (Succ Zero)) (Succ Zero)
Add (Succ (Succ Zero)) (Succ Zero) :: Nat

λ> :kind! Add (Succ (Succ Zero)) (Succ Zero)
Add (Succ (Succ Zero)) (Succ Zero) :: Nat
= 'Succ ('Succ ('Succ 'Zero))

file4.txt

data Maybe a
    = Just a
    | Nothing

file40.txt

append :: Vector n a -> Vector m a -> Vector (Add n m) a

file41.txt

append VNil rest = VNil

file42.txt

    • Could not deduce: m ~ 'Zero
      from the context: n ~ 'Zero
        bound by a pattern with constructor:
                   VNil :: forall a. Vector 'Zero a,
                 in an equation for ‘append’
        at /home/matt/Projects/dep-types.hs:31:8-11
      ‘m’ is a rigid type variable bound by
        the type signature for:
          append :: forall (n :: Nat) a (m :: Nat).
                    Vector n a -> Vector m a -> Vector (Add n m) a
        at /home/matt/Projects/dep-types.hs:30:11
      Expected type: Vector (Add n m) a
        Actual type: Vector 'Zero a
    • In the expression: VNil
      In an equation for ‘append’: append VNil rest = VNil
    • Relevant bindings include
        rest :: Vector m a
          (bound at /home/matt/Projects/dep-types.hs:31:13)
        append :: Vector n a -> Vector m a -> Vector (Add n m) a
          (bound at /home/matt/Projects/dep-types.hs:31:1)

file43.txt

λ> :t append VNil
append VNil :: Vector m a -> Vector m a

file44.txt

append VNil xs = xs

file45.txt

append (VCons a rest) xs = append rest (VCons a xs)

file46.txt

λ> append (VCons 1 (VCons 3 VNil)) (VCons 2 VNil)
VCons 3 (VCons 1 (VCons 2 (VNil)))

file47.txt

append (VCons a rest) xs = VCons a (append rest xs)

file48.txt

λ> :reload
[1 of 1] Compiling DepTypes         ( /home/matt/Projects/dep-types.hs, interpreted )

/home/matt/Projects/dep-types.hs:32:28: error:
    • Could not deduce: Add n1 ('Succ m) ~ 'Succ (Add n1 m)
      from the context: n ~ 'Succ n1
        bound by a pattern with constructor:
                   VCons :: forall a (n :: Nat).
                            a -> Vector n a -> Vector ('Succ n) a,
                 in an equation for ‘append’
        at /home/matt/Projects/dep-types.hs:32:9-20
      Expected type: Vector (Add n m) a
        Actual type: Vector ('Succ (Add n1 m)) a
    • In the expression: VCons a (append rest xs)
      In an equation for ‘append’:
          append (VCons a rest) xs = VCons a (append rest xs)
    • Relevant bindings include
        xs :: Vector m a (bound at /home/matt/Projects/dep-types.hs:32:23)
        rest :: Vector n1 a
          (bound at /home/matt/Projects/dep-types.hs:32:17)
        append :: Vector n a -> Vector m a -> Vector (Add n m) a
          (bound at /home/matt/Projects/dep-types.hs:31:1)
Failed, modules loaded: none.

file49.txt

data Vector n a where
    VNil :: Vector Zero a
    VCons :: a -> Vector n a -> Vector (Succ n) a

type family Add x y where
    Add 'Zero n = n
    Add ('Succ n) m = Add n ('Succ m)

append :: Vector n a -> Vector m a -> Vector (Add n m) a
append VNil xs           = xs
append (VCons a rest) xs = VCons a (append rest xs)

file5.txt

λ> :t Just
Just :: a -> Maybe a
λ> :t Nothing
Nothing :: Maybe a

file50.txt

append (VCons a rest) xs = VCons a (append rest xs)

file51.txt

type family Add x y where
  Add 'Zero n     = n
  Add ('Succ n) m = 'Succ (Add n m)

file52.txt

{-# LANGUAGE TypeOperators #-}

file53.txt

data HList xs where
    HNil :: HList '[]
    (:::) :: a -> HList as -> HList (a ': as)

infixr 6 :::

file54.txt

λ> :t 'a' ::: 1 ::: "hello" ::: HNil
'a' ::: 1 ::: "hello" ::: HNil 
    :: HList '[Char, Int, String]

file55.txt

λ> 'a' ::: 1 ::: "hello" ::: HNil

\<interactive\>:13:1:
    No instance for (Show (HList '[Char, Int, String]))
      arising from a use of ‘print’
    In the first argument of ‘print’, namely ‘it’
    In a stmt of an interactive GHCi command: print it

file56.txt

instance Show (HList xs) where
    show HNil         = "HNil"
    show (x ::: rest) = "_ ::: " ++ show rest

file57.txt

instance Show (HList '[]) where
    show HNil         = "HNil"

file58.txt

{-# LANGUAGE FlexibleInstances #-}

file59.txt

{-# LANGUAGE FlexibleContexts #-}

file6.txt

λ> let nothingA = Nothing :: Maybe a
λ> let nothingInt = Nothing :: Maybe Int
λ> let nothingChar = Nothing :: Maybe Char
λ> nothingInt == nothingChar

\<interactive\>:27:15: error:
    • Couldn't match type ‘Char’ with ‘Int’
      Expected type: Maybe Int
        Actual type: Maybe Char
    • In the second argument of ‘(==)’, namely ‘nothingChar’
      In the expression: nothingInt == nothingChar
      In an equation for ‘it’: it = nothingInt == nothingChar
λ> nothingA == nothingInt
True
λ> nothingA == nothingChar
True

file60.txt

instance (Show (HList as), Show a) 
    => Show (HList (a ': as)) where
    show (a ::: rest) = 
        show a ++ " ::: " ++ show rest

file61.txt

λ> 'a' ::: 1 ::: "hello" ::: HNil
'a' ::: 1 ::: "hello" ::: HNil

file62.txt

{-# LANGUAGE PolyKinds        #-}
{-# LANGUAGE TypeApplications #-}

file63.txt

newtype s >> a = Named a

data HRec xs where
  HEmpty :: HRec '[]
  HCons  :: (s >> a) -> HRec xs -> HRec (s >> a ': xs)

file64.txt

λ> HCons (Named @"foo" 'a') (HCons (Named @"bar" (3 :: Int)) HEmpty)

\<interactive\>:10:1: error:
    • No instance for (Show (HRec '["foo" >> Char, "bar" >> Int]))
        arising from a use of ‘print’
    • In a stmt of an interactive GHCi command: print it

file65.txt

λ> :t symbolVal
-- proxyを受け取って、その型をStringとして返す
symbolVal :: KnownSymbol n => proxy n -> String
λ> let a = (Proxy :: Proxy "hello")
λ> symbolVal a
"hello"

file66.txt

instance Show (HRec '[]) where
  show _ = "HEmpty"

file67.txt

instance Show (HRec (s >> a ': xs)) where

file68.txt

instance Show (HRec (s >> a ': xs)) where
    show (HCons (Named a) rest) =

file69.txt

instance (Show a) 
    => Show (HRec (s >> a ': xs)) where
    show (HCons (Named a) rest) =
        let val = show a

file7.txt

λ> :type Maybe

\<interactive\>:1:1: error:
    • Data constructor not in scope: Maybe
    • Perhaps you meant variable ‘maybe’ (imported from Prelude

file70.txt

instance (Show a, KnownSymbol s) 
    => Show (HRec (s >> a ': xs)) where
    show (HCons (Named a) rest) =
        let val = show a
            key = symbolVal (Proxy :: Proxy s)

file71.txt

topLevelFunction :: a -> (a -> b) -> b
topLevelFunction a = go
  where
    go :: (a -> b) -> b
    go f = f a

file72.txt

topLevelFunction :: a0 -> (a0 -> b0) -> b0
topLevelFunction a = go
  where
    go :: (a1 -> b1) -> b1
    go f = f a

file73.txt

{-# LANGUAGE ScopedTypeVariables #-}

file74.txt

instance (Show a, KnownSymbol s, Show (HRec xs)) 
    => Show (HRec (s >> a ': xs)) where
    show (HCons (Named a) rest) =
        let val = show a
            key = symbolVal (Proxy :: Proxy s)
            more = show rest
         in "(" ++ key ++ ": " ++ val ++ ") " ++ more

file75.txt

λ> HCons (Named @"foo" 'a') (HCons (Named @"bar" (3 :: Int)) HEmpty)
(foo: 'a') (bar: 3) HEmpty

file8.txt

λ> :kind Maybe
Maybe :: * -> *

file9.txt

λ> :kind Maybe
Maybe :: * -> *