大家好, 小弟也是對於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)