Михаил Ильин ([info]yorool_gui) wrote in [info]ru_lambda,
@ 2007-10-10 20:47:00
Previous Entry  Add to memories!  Tell a Friend!  Next Entry
что значит data ... where
Объясните pls, что значит вот это (отсюда):

data Rigidity m where
    Rigid :: Rigidity Maybe
    Flexible :: Rigidity Identity

Я такого синтаксиса раньше не встречал. Он где описан?

(Post a new comment)


[info]deni_ok
2007-10-10 05:00 pm UTC (link)
Это GADTы (Generalised Algebraic Datatype):

http://www.rsdn.ru/Forum/?mid=2567908

там есть ссылки на первоисточники.

(Reply to this)


[info]lomeo
2007-10-10 07:06 pm UTC (link)
GADT.

Вкратце, обычные конструкторы данных имеют типы, которые выводятся из их параметров и конструктора типа. Причём эти типы наиболее общие:

data [a] = [] | a : [a]

-- значит, конструкторы имеют типы
[] :: [a]
(:) :: a -> [a] -> [a]

data Maybe a = Nothing | Just a

Nothing :: Maybe a
Just :: a -> Maybe a


GADT позволяет указывать типы явно:

data [a] where
    []  :: [a]
    (:) :: a -> [a] -> [a]

data Maybe a where
    Nothing :: Maybe a
    Just    :: a -> Maybe a



В случае GADT также мы можем указать более специфические типы. В твоём примере это

Rigid :: Rigidity Maybe
Flexible :: Rigidity Identity


Нужно это для увеличения возможностей по ограничению типа. Например, при описании GADT часто приводят пример с типом выражения, где конструкторы могут иметь, например, такие типы:

data Exp :: * -> * where
    Plus :: Exp Int -> Exp Int -> Exp Int -- может принимать только выражения с Int и возвращает такой же
    Not  :: Exp Bool -> Exp Bool -- аналогично, кроме как выражения над логическими значениями смысла не имеет.

(Reply to this)

Create an Account
Forgot your login or password?
Login w/ OpenID
English • Español • Deutsch • Русский…