Famiglie di tipi chiusi e tipi di funzione sconosciuti

Question

Scusate, non potrei immaginare alcun titolo migliore per la domanda, quindi leggete in anticipo. Immaginate di avere un tipo di famiglia chiuso che associa ogni tipo ad esso è corrispondente Maybe tranne se stessi maybes:

type family Family x where 
    Family (Maybe x) = Maybe x 
    Family x = Maybe x 

Possiamo anche dichiarare una funzione che utilizza quel tipo di famiglia:

doMagic :: a -> Family a 
doMagic = undefined 

exampleA = doMagic $ Just() 
exampleB = doMagic $() 

Giocando con esso in GHCi dimostra che è ok per valutare il tipo di questa applicazione funzione:

*Strange> :t exampleA  
exampleA :: Maybe()  
*Strange> :t exampleB  
exampleB :: Maybe()  

la domanda è se è possibile prevedere eventuali implementati sulla funzione doMagic eccetto undefined? Diciamo per esempio che mi piacerebbe racchiudere ogni valore in un costruttore Just, ad eccezione di Maybes che dovrebbe rimanere intatto, come potrei farlo? Ho provato a utilizzare i typeclass, ma non sono riuscito a scrivere una firma compilabile per la funzione doMagic se non si utilizzano famiglie di tipo chiuso, qualcuno potrebbe aiutarmi per favore?

Answer 1

È possibile utilizzare un altro tipo di famiglia chiusa per distinguere Maybe x da x e quindi è possibile utilizzare un altro typeclass per fornire implementazioni separate di doMagic per questi due casi.Versione rapida e sporca:

{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, 
    FlexibleInstances, UndecidableInstances, ScopedTypeVariables #-} 

type family Family x where 
    Family (Maybe x) = Maybe x 
    Family x = Maybe x 

data True 
data False 

type family IsMaybe x where 
    IsMaybe (Maybe x) = True 
    IsMaybe x = False 


class DoMagic a where 
    doMagic :: a -> Family a 

instance (DoMagic' (IsMaybe a) a (Family a)) => DoMagic a where 
    doMagic = doMagic' (undefined :: IsMaybe a) 


class DoMagic' i a r where 
    doMagic' :: i -> a -> r 

instance DoMagic' True (Maybe a) (Maybe a) where 
    doMagic' _ = id 

instance DoMagic' False a (Maybe a) where 
    doMagic' _ = Just 


exampleA = doMagic $ Just() 
exampleB = doMagic $() 

Answer 2

È possibile effettuare una sorta di funzione doMagic che va in pausa. Sfortunatamente, la chiusura della famiglia tipo non ti aiuta molto. Ecco come un inizio potrebbe apparire

{-# LANGUAGE TypeFamilies #-} 

type family Family x where 
    Family (Maybe x) = Maybe x 
    Family x = Maybe x 

class Magical a where doMagic :: a -> Family a 
instance Magical (Maybe a) where doMagic = id 
instance Magical() where doMagic = Just 

si può vedere lavorare in ghci proprio come lei ha chiesto:

*Main> doMagic $ Just() 
Just() 
*Main> doMagic $() 
Just() 

Allora perché io dico che è zoppicando lungo? Bene, avrete notato che i due casi previsti non coprono molto dell'ecosistema Haskell di tipi:

*Main> doMagic $ True 
<interactive>:3:1: 
    No instance for (Magical Bool) arising from a use of ‘doMagic’ 
    In the expression: doMagic 
    In the expression: doMagic $ True 
    In an equation for ‘it’: it = doMagic $ True 

Così uno avrebbe dovuto fornire le istanze per ogni tipo (costruttore) di interesse. In effetti, nemmeno le istanze incoerenti - il club con cui molti di questi problemi possono essere battuti in sottomissione - aiuta qui; se si cerca di scrivere

instance Magical (Maybe a) where doMagic = id 
instance Magical a where doMagic = Just 

il compilatore si lamenta giustamente che dopo tutto non sappiamo che l'istanza completamente polimorfica ha in realtà il tipo giusto. Il problema delle istanze incoerenti è che il compilatore non ci ha detto che, proprio perché è stata scelta l'istanza, che le altre istanze sicuramente non si applicano a. Quindi è possibile che scegliamo l'istanza completamente polimorfa a un certo punto, solo per scoprire in seguito che eravamo davvero uno Maybe dietro le quinte, e quindi abbiamo appena avvolto uno o più strati di Maybe attorno a cose. Sfortunato.

Al momento non si può fare molto. Le famiglie di tipo chiuso al momento non forniscono tutte le conoscenze che si potrebbero desiderare di avere a disposizione. Forse un giorno GHC offrirà un meccanismo che rende le famiglie di tipo chiuso più utili a questo proposito, come un vincolo di disuguaglianza di tipo, ma non terrei il respiro: è un problema di ricerca come fornire queste informazioni utili, e io non ho Ho sentito voci di persone che lo affrontano.