È possibile avere sinonimi di tipo smemorato in Haskell?

Question

Se ho un tipo con un parametro fantasma che ho solo qualche volta a cuore, come questo:

data Foo p a b = Bar a b 

C'è un modo hack per scrivere un tipo sinonimo Baz tale che Baz a b è Foo p a b per qualche p che ho hai dimenticato?

Non si può fare:

type Baz a b = Foo p a b 

e mentre si può fare (con estensioni appropriate):

type Baz a b = forall p.Foo p a b 

Non sembra così fa quello che voglio, perché non posso convertire un valore di tipo Foo P1 a b in tipo Baz a b, con un messaggio relativo a una "variabile di tipo rigido".

Avete bisogno di un altro strato di controli per ottenere questo effetto, come di seguito? Potresti spiegare brevemente perché?

data Baz' a b = forall p.Baz' (Foo p a b) 

Answer 1

Attualmente non esiste un modo per farlo come sinonimo di tipo. Tuttavia, se si dispone di GHC 7.10, è possibile attivare l'estensione PartialTypeSignatures e scrivere invece Foo _ a b. Usa -fno-warn-partial-type-signatures per chiedere a GHC di non avvisarti su ciascuna delle buche che lasci in questo modo.

Answer 2

Questo non può essere fatto in modo affidabile con i sinonimi di tipo. Hai bisogno di tipi esistenziali o di rango-n tipi.

Il problema è che Haskell consente ai sinonimi di tipo di essere completamente intersubituibili. Ad esempio, quando si definisce type Baz a b = Foo p a b, in ogni contesto in cui si dispone di Foo p a b, è possibile utilizzare Baz a b e viceversa. Così, per esempio, se si ha una funzione di questo tipo:

f1 :: Foo Something a b -> Whatever Something b a 

Poi a causa della sostituibilità, che sarebbe lo stesso tipo come questo:

f1 :: Baz a b -> Whatever Something b a 

E come questo:

f1 :: Foo p a b -> Whatever Something b a 

... che poi si potrebbe specializzarsi in questo:

f1 :: Foo SomethingElse a b -> Whatever Something b a 

Quindi, cosa puoi fare? Uno è quello di definire un tipo di involucro esistenziale:

{-# LANGUAGE ExistentialTypes #-} 

data Baz a b = forall p. Baz (Foo p a b) 

modo alternativo di fare la stessa cosa:

{-# LANGUAGE GADTs #-} 

data Baz a b where 
    Baz :: Foo p a b -> Baz a b 

Secondo modo si potrebbe andare: tipi rango-N e stile continuazione-passing:

{-# LANGUAGE RankNTypes #-} 

-- To consume one of these, you pass a "callback" function to `runBaz`, 
-- which is not allowed to restrict the type variable `p`. 
newtype Baz a b = Baz { runBaz :: forall p r. (Foo p a b -> r) -> r } 

makeBaz :: Foo p a -> Baz a b 
makeBaz foo = Baz ($foo) 

Terzo modo, che hai tentato e (mi hanno detto) non funziona molto bene: digita sinonimi + tipi impredicativi (che sono necessari per ottenere i sinonimi di forall come argomenti di tipo in molti casi).