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