Haskellで型レベルプログラミングで遊ぶ
Haskellで型レベルプログラミング
型のみの計算をする ref
pre.hs>>> :set -XFlexibleContexts
>>> :type undefined :: HasDefault Bool => BoolFlexibleContextsをsetしたあとに、
undefiend に対して目的の型注釈をする超良記事
キーワード
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に関するもろもろの紹介
>#WIP
依存型で型依存Neural Networkを作る