जीएडीटी बनाम मल्टीपार्म टाइप टाइप

Question

मैं GADTs को समझने की कोशिश कर रहा हूं, और मैंने जीएचसी के मैनुअल में GADTs example को देखा है। जहाँ तक मेरा बता सकते हैं, यह MultiParamTypeClasses साथ एक ही बात करने के लिए संभव है:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, 
    FlexibleInstances, UndecidableInstances #-} 

class IsTerm a b | a -> b where 
    eval :: a -> b 

data IntTerm = Lit Int 
       | Succ IntTerm 
data BoolTerm = IsZero IntTerm 
data If p a = If p a a 
data Pair a b = Pair a b 

instance IsTerm IntTerm Int where 
    eval (Lit i)  = i 
    eval (Succ t)  = 1 + eval t 

instance IsTerm BoolTerm Bool where 
    eval (IsZero t) = eval t == 0 

instance (IsTerm p Bool, IsTerm a r) => IsTerm (If p a) r where 
    eval (If b e1 e2) = if eval b then eval e1 else eval e2 

instance (IsTerm a c, IsTerm b d) => IsTerm (Pair a b) (c, d) where 
    eval (Pair e1 e2) = (eval e1, eval e2) 

ध्यान दें, हम ठीक उसी निर्माणकर्ता और eval के लिए ठीक उसी कोड है (प्रसार पार उदाहरण परिभाषाओं) में के रूप में है कि जीएचसी का GADTs उदाहरण।

तो GADTs के बारे में सभी फ़ज़ क्या है? क्या कोई ऐसी चीज है जो मैं GADTs के साथ कर सकता हूं कि मैं MultiParamTypeClasses के साथ नहीं कर सकता? या क्या वे सिर्फ उन चीजों को करने का एक संक्षिप्त तरीका प्रदान करते हैं जिन्हें मैं MultiParamTypeClasses के साथ कर सकता हूं?

Answer 1

आप एक ही प्रकार के हैं, लेकिन एक कंटेनर सुविधा में विभिन्न निर्माताओं के साथ GADT मूल्यों डाल सकते हैं,

map eval [Lit 1, If (IsZero (Lit 3)) (Lit 4) (Succ (Lit 6))] 

कार्यात्मक निर्भरता के साथ अलग-अलग प्रकार और MPTCs का उपयोग कर सीधा है, लेकिन एक ही प्राप्त करने के लिए कम से कम मुश्किल है । आपके मल्टीपार्मामीटर प्रकार वर्ग दृष्टिकोण में, Lit और If विभिन्न प्रकार के निर्माता हैं, इसलिए उन्हें एक ही कंटेनर में रखने के लिए एक रैपर प्रकार की आवश्यकता होगी। आवरण प्रकार होता है, जहाँ तक मैं देख सकते हैं, एक

instance IsTerm (Wrap t) t where 
    eval (Wrapper e) = eval e 

साथ ला

data Wrap t = forall a. (IsTerm a t) => Wrapper a 

एक अस्तित्व प्रकार होना eval से अधिक की तरह कुछ प्रकार की सुरक्षा और map कार्यों की क्षमता सुनिश्चित करने के लिए है सूचि। तो आप सुविधा को घटाकर, जीएडीटी के आधे रास्ते या अधिक वापस आ गए हैं।

मुझे यकीन नहीं है कि कुछ भी है GADT आपको ऐसा करने की अनुमति देता है कि आप उनके बिना हासिल नहीं कर सकते हैं, लेकिन कुछ चीजें बलिदान के को बलिदान देगी।

Answer 2

GADTs सिर्फ आपको कन्स्ट्रक्टर परिभाषित करने का अधिक प्राकृतिक तरीका प्रदान करने की अनुमति देता है और सभी प्रकार के स्तर और कन्स्ट्रक्टरों पर मिलान करने की अनुमति देता है (ऐसा कुछ है जिसे आप इसके बिना नहीं कर सकते हैं, मुझे लगता है)।

{-# LANGUAGE GADTs #-} 
data Term a = (a ~ Bool) => IsZero (Term Int) 
      | (a ~ Int) => Lit Int 
eval :: Term a -> a 
eval (IsZero t) = eval t == 0 
eval (Lit a) = a