Haskellで型レベルプログラミングで遊ぶ

型のみの計算をする ref

code:pre.hs

>> :set -XFlexibleContexts

>> :type undefined :: HasDefault Bool => Bool

FlexibleContextsをsetしたあとに、undefiendに対して目的の型注釈をする

超良記事mrsekut.icon

キーワード

code:hs

{-# LANGUAGE DataKinds #-}

{-# LANGUAGE GADTs #-}

{-# LANGUAGE TypeFamilies #-}

{-# LANGUAGE UndecidableInstances #-}

data Nat = Zero | Succ Nat

data Vector (n :: Nat) (a :: *) where

VNil ::Vector 'Zero a

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

instance Show a => Show (Vector n a) where

show VNil = "VNil"

show (VCons a as) = "VCons " ++ show a ++ " (" ++ show as ++ ")"

type family Add x y where

Add 'Zero n = n

Add ('Succ n) m = 'Succ (Add n 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)

kindに関するもろもろの紹介