[問題] GADT 概念
大家好, 小弟也是對於FL跟PL理論有一些興趣的人
最近讀了一下什麼是GADT
http://www.haskell.org/haskellwiki/Generalised_algebraic_datatype
http://hackage.haskell.org/trac/haskell-prime/wiki/GADTs
http://hackage.haskell.org/trac/haskell-prime/wiki/ExistentialQuantification
看了以上三篇文章,不確定是不是真的懂
所以說GADT在Haskell上面給我們一種方式去定義generic type可以包含其他的type?
ex:
data Parser tok a where
Zero :: Parser tok ()
One :: Parser tok ()
Check :: (tok -> Bool) -> Parser tok tok
Satisfy :: ([tok] -> Bool) -> Parser tok [tok]
Push :: tok -> Parser tok a -> Parser tok a
Plus :: Parser tok a -> Parser tok b -> Parser tok (Either a b)
Times :: Parser tok a -> Parser tok b -> Parser tok (a,b)
Star :: Parser tok a -> Parser tok [a]
otherwise we need to write something like this (separate the type and
functions):
newtype Parser tok a
zero::Parser tok ()
one :: Parser tok ()
謝謝~
p.s
看到一個寫法, 不知道這樣算不算是dependent type的一種應用XD
利用type讓head function不用檢查是不是nil
data Empty
data NonEmpty
data List x y where
Nil :: List a Empty
Cons:: a -> List a b -> List a NonEmpty
safeHead:: List x NonEmpty -> x
safeHead (Cons a b) = a
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 85.224.79.33
※ 編輯: command 來自: 85.224.79.33 (11/28 03:05)
推
11/28 20:58, , 1F
11/28 20:58, 1F
推
11/28 21:10, , 2F
11/28 21:10, 2F
討論串 (同標題文章)
PLT 近期熱門文章
PTT數位生活區 即時熱門文章
