बंद प्रकार के परिवारों पर बाधाएं?

Question

मैं प्रकार की एक समारोह के एक बुरी तरह गैर पैरामीट्रिक संस्करण लिखने के लिए

pretty :: (Show a) => a -> Text 

ऐसी है कि

pretty :: Text -> Text = id 
pretty :: String -> Text = T.pack 
pretty :: (Show a) => a -> Text = T.pack . show 

तो विचार है कि कुछ भी पहले से ही एक Show उदाहरण है कि चालू किया जा सकता है करना चाहते हैं Text और String को छोड़कर, जिसे हम विशेष मामले चाहते हैं, को छोड़कर show द्वारा "सुंदर" Text में।

निम्नलिखित कोड काम करता है:

{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE MultiParamTypeClasses #-} 
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, FlexibleContexts #-} 
{-# LANGUAGE DataKinds, ConstraintKinds #-} 
module Pretty (pretty) where 

import Data.Text (Text) 
import qualified Data.Text as T 

type family StringLike a :: Bool where 
    StringLike String = True 
    StringLike Text = True 
    StringLike a = False 

class (b ~ StringLike a) => Pretty' a b where 
    pretty' :: a -> Text 

instance Pretty' String True where 
    pretty' = T.pack 

instance Pretty' Text True where 
    pretty' = id 

instance (Show a, StringLike a ~ False) => Pretty' a False where 
    pretty' = T.pack . show 

type Pretty a = (Pretty' a (StringLike a)) 

pretty :: (Pretty a) => a -> Text 
pretty = pretty' 

और यह pretty समारोह के अलावा कुछ निर्यात के बिना इस्तेमाल किया जा सकता।

हालांकि, मैं pretty के लिए प्रकार हस्ताक्षर के बारे में भी खुश नहीं हूँ:

pretty :: (Pretty a) => a -> Text 

मुझे लगता है कि जब से StringLike एक बंद प्रकार परिवार है, वहाँ एक रास्ता GHC यह पता लगाने के लिए किया जाना चाहिए कि अगर केवल (Show a) रखती है, (Pretty a) पहले से ही संतुष्ट हो जाता है, के बाद से:

1. The following hold trivially just by substituting the results of applying StringLike: 
(StringLike String ~ True, Pretty' String True) 
(StringLike Text ~ True, Pretty' Text True) 

2. For everything else, we *also* know the result of applying StringLike: 
(Show a, StringLike a ~ False) => (Pretty' a (StringLike a)) 

वहाँ इस के GHC को समझाने के लिए कोई तरीका है?

Answer 1

मुझे लगता है कि जब से StringLike एक बंद प्रकार परिवार है, वहाँ एक रास्ता GHC यह पता लगाने के लिए कि अगर केवल (Show a) रखती है, (Pretty a) पहले से ही संतुष्ट है

ऐसा करने के लिए उस प्रकार निरीक्षण की आवश्यकता होगी होना चाहिए , और पैरामीटर संबंधी बहुरूपता तोड़ देगा। अपने तर्क से अब एक प्रकार परिवार

type family IsInt a :: Bool where 
    IsInt Int = True 
    IsInt a = False 
class (b ~ IsInt a) => TestInt a b where 
    isInt :: a -> Bool 
instance TestInt Int True where 
    isInt _ = True 
instance (IsInt a ~ False) => TestInt a False where 
    isInt _ = False 

को परिभाषित करने पर विचार करें, GHC () से TestInt a को पूरा करने के लिए सक्षम होना चाहिए। दूसरे शब्दों में, हम किसी दिए गए प्रकार के लिए परीक्षण करने में सक्षम होना चाहिए चाहे वह इंट के बराबर हो। यह स्पष्ट रूप से असंभव है।

इसी तरह, Show a शब्दकोश एक समारोह a -> ShowS के समतुल्य है। आप निर्णय लेने में सक्षम कैसे होंगे, केवल यह देखते हुए कि क्या तर्क StringLike है?

Answer 2

शायद मैंने आपके लक्ष्य को गलत समझा लेकिन यह आपके इच्छित प्रकार को पाने के लिए बहुत सारे काम की तरह लगता है।

{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, UndecidableInstances, IncoherentInstances #-} 
module Prettied where 

import Data.Text (Text, pack) 

class Pretty a where pretty :: a -> Text 

instance   Pretty Text where pretty = id 
instance   Pretty String where pretty = pack 
instance Show a => Pretty a  where pretty = pack . show 

यह लग सकता है जबकि उस pretty, प्रकार Pretty a => a -> Text होना चाहिए की वजह से IncoherentInstances यह वास्तव में प्रकार Show a => a -> Text होगा। यह शायद अपने मॉड्यूल में होना चाहिए क्योंकि IncoherentInstances सक्षम करना उन चीजों में से एक है जो वैध कोड तोड़ सकते हैं।