Type Level Literals - İkili işlevde farklı yazılan parametreler kullanılamıyor

Question

Belki gibi bir tür kullanarak boş olmayan kap değerlerini (fantom türlerinde olduğu gibi) ayırt etmenin bir yolu olarak Type Level Literals ile oynuyor.

Bu iyi çalışıyor. (Gerekli GHC> = 7.6.1)

Ancak ikili bir işlev tanımlamak için çalışırken değerler farklı grupları kabul eder (eşdeğer)

eq :: (Eq a) => TMaybe (sym :: Symbol) a -> TMaybe (sym :: Symbol) a -> Bool 

, kullanıldığı bir derleme hata sinyali gönderir:

senin tipin, tip "Just"' with "Hiçbir şey"'

{-# LANGUAGE DataKinds, KindSignatures, GADTs, FlexibleInstances #-} 

import GHC.TypeLits 

data TMaybe :: Symbol -> * -> * where 
    TNothing :: TMaybe "Nothing" a 
    TJust :: a -> TMaybe "Just" a 

nonEmpty :: Maybe a -> TMaybe "Just" a 
nonEmpty (Just x) = TJust x 
nonEmpty Nothing = error "invalid nonEmpty data" 

-- this fromJust rejects TNothing at compile time 
fromJust :: (sym ~ "Just") => TMaybe (sym :: Symbol) a -> a 
fromJust (TJust x) = x 

tmbToMaybe :: TMaybe (sym :: Symbol) a -> Maybe a 
tmbToMaybe TNothing = Nothing 
tmbToMaybe (TJust x) = Just x 

mbToTNothing Nothing = TNothing 

mbToTJust (Just x) = TJust x 

instance Eq a => Eq (TMaybe (sym :: Symbol) a) where 
    TNothing == TNothing = True 
    TJust x == TJust y = x == y 
    _ == _ = False -- useless, equal types required 

instance Ord a => Ord (TMaybe (sym :: Symbol) a) where 
    compare TNothing TNothing = EQ 
    compare (TJust x) (TJust y) = Prelude.compare x y 
    compare TNothing _ = LT -- useless, equal types required 
    compare _ TNothing = GT -- useless, equal types required 

instance Functor (TMaybe (sym :: Symbol)) where 
    fmap _ TNothing  = TNothing 
    fmap f (TJust a)  = TJust (f a) 

instance Monad (TMaybe "Just") where 
    (TJust x) >>= k  = k x 

    (TJust _) >> k  = k 

    return   = TJust 
    fail _    = error "can't fail to TNothing" 

-------------------------- 

-- defining eq to admit parameter types with different symbol 

eq :: (Eq a) => TMaybe (sym :: Symbol) a -> TMaybe (sym :: Symbol) a -> Bool 
eq TNothing TNothing = True 
eq (TJust x) (TJust y) = x == y 
eq _ _ = False 

--------------------------- 

-- Test 

main = do 
     print $ fromJust $ TJust (5::Int) -- type-checks 
     -- print $ fromJust TNothing -- as expected, does not type-check 

     -- print $ TNothing == TJust (5::Int) -- as expected, does not type-check, types required equal at function def. 
     print $ TNothing `eq` TJust (5::Int) -- does not type-check either 

Answer 1

Eh ulaşamasa

eq :: (Eq a) => TMaybe (sym :: Symbol) a -> TMaybe (sym :: Symbol) a -> Bool 

, her iki bağımsız değişkenin de aynı tür olduğunu iddia eder, dolayısıyla derleyici, TMaybe "Nothing" a ve TMaybe "Just" a'u karşılaştırmaya yönelik bir girişimi reddeder. Eğer

eq :: (Eq a) => TMaybe (sym :: Symbol) a -> TMaybe (sym1 :: Symbol) a -> Bool 

o derler ve

için türünü değiştirirseniz

TNothing `eq` TJust (5::Int) 

False olarak değerlendirilir. (Daha sonra, birçok yerde TNothing s türünü açıkça belirtmeniz gerekir.)