क्या हैकेल प्रकार चर पर असमानता बाधा डालना संभव है?

Question

क्या में GHC type family docs में समानता के बजाय असमानता को छोड़कर, एक कार्य के प्रकार के उपन्यासों पर असमानता बाधा डालना संभव है?

मुझे एहसास है कि ऐसा करने का कोई प्रत्यक्ष तरीका नहीं है (क्योंकि ghc दस्तावेज़ मेरे ज्ञान में कोई भी सूचीबद्ध नहीं है), लेकिन मैं लगभग परेशान होगा अगर यह सभी के प्रकाश में किसी भी तरह से संभव नहीं था विदेशी प्रकार-फू का खुलासा किया गया है।

Answer 1

सबसे पहले, ध्यान रखें कि विशिष्ट प्रकार चर पहले से ही उनके दायरे में गैर-अक्षम हैं - उदाहरण के लिए, यदि आपके पास \x y -> x है, तो इसे टाइप हस्ताक्षर a -> b -> c कठोर प्रकार चर से मिलान करने में सक्षम नहीं होने के बारे में एक त्रुटि उत्पन्न करेगा। तो यह केवल फ़ंक्शन को कॉल करने वाली किसी भी चीज़ पर लागू होगा, इसे अन्यथा सरल पॉलिमॉर्फिक फ़ंक्शन का उपयोग करने से रोकने के लिए जो दो प्रकार के बराबर होगा। यह कुछ इस तरह काम करेगा, मुझे लगता है:

const' :: (a ~/~ b) => a -> b -> a 
const' x _ = x 

foo :: Bool 
foo = const' True False -- this would be a type error 

निजी तौर पर मुझे शक है यह वास्तव में उपयोगी होगा - प्रकार चर की स्वतंत्रता को पहले से ही, कुछ तुच्छ करने के लिए टूट दो प्रकार जानने से सामान्य कार्यों से बचाता है असमान हैं नहीं है असल में आप कुछ भी दिलचस्प करते हैं (समानता के विपरीत, जो आपको दो प्रकारों के बीच सहभागिता देता है), और ऐसी चीजें सशर्त साधनों की बजाय घोषणात्मक होती हैं कि आप इसे किसी प्रकार की विशेषज्ञता तकनीक के हिस्से के बराबर/असमान के बीच अंतर करने के लिए उपयोग नहीं कर सकते ।

तो, यदि आपके मन में कुछ विशिष्ट उपयोग है जहां आप इसे चाहते हैं, तो मैं एक अलग दृष्टिकोण की कोशिश करने का सुझाव दूंगा।

दूसरी ओर, अगर आप सिर्फ हास्यास्पद प्रकार hackery साथ खेलने के लिए चाहते हैं ...

{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE FlexibleContexts #-} 
{-# LANGUAGE FlexibleInstances #-} 
{-# LANGUAGE FunctionalDependencies #-} 
{-# LANGUAGE MultiParamTypeClasses #-} 
{-# LANGUAGE UndecidableInstances #-} 
{-# LANGUAGE OverlappingInstances #-} 

-- The following code is my own hacked modifications to Oleg's original TypeEq. Note 
-- that his TypeCast class is no longer needed, being basically equivalent to ~. 

data Yes = Yes deriving (Show) 
data No = No deriving (Show) 

class (TypeEq x y No) => (:/~) x y 
instance (TypeEq x y No) => (:/~) x y 

class (TypeEq'() x y b) => TypeEq x y b where 
    typeEq :: x -> y -> b 
    maybeCast :: x -> Maybe y 

instance (TypeEq'() x y b) => TypeEq x y b where 
    typeEq x y = typeEq'() x y 
    maybeCast x = maybeCast'() x 

class TypeEq' q x y b | q x y -> b where 
    typeEq' :: q -> x -> y -> b 
    maybeCast' :: q -> x -> Maybe y 

instance (b ~ Yes) => TypeEq'() x x b where 
    typeEq'() _ _ = Yes 
    maybeCast' _ x = Just x 

instance (b ~ No) => TypeEq' q x y b where 
    typeEq' _ _ _ = No 
    maybeCast' _ _ = Nothing 

const' :: (a :/~ b) => a -> b -> a 
const' x _ = x 

ठीक है, कि अविश्वसनीय रूप से मूर्ख था। काम करता है, हालांकि:

> const' True() 
True 
> const' True False 

<interactive>:0:1: 
    Couldn't match type `No' with `Yes' 
    (...) 

Answer 2

जीएचसी 7.8.1 से। closed type families are available। समाधान उनके साथ बहुत आसान है:

data True 
data False 

type family TypeEqF a b where 
    TypeEqF a a = True 
    TypeEqF a b = False 

type TypeNeq a b = TypeEqF a b ~ False