2016-05-31 15 views
7

Sto esplorando famiglie di tipi in Haskell, cercando di stabilire la complessità delle funzioni a livello di tipo che posso definire. Voglio definire una versione chiusa tipo a livello di mod, qualcosa in questo modo:Vincoli nelle istanze di tipo famiglia

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-} 
import GHC.TypeLits 

type family Mod (m :: Nat) (n :: Nat) :: Nat where 
    n <= m => Mod m n = Mod (m - n) n 
    Mod m n = m 

Tuttavia, il compilatore (GHC 7.10.2) respinge questa, come il vincolo nella prima equazione non è permesso. In che modo le guardie a livello di valore si traducono in livello di testo? Questo è ancora possibile in Haskell attualmente?

+0

Forse c'è una funzione di livello di tipo 'Se'? Penso di averlo visto da qualche parte, ma non sono un esperto di biblioteca ... – chi

+0

Grazie, hai perfettamente ragione, "Se" esiste in [Data.Type.Bool] (https://hackage.haskell.org /package/base/docs/Data-Type-Bool.html). –

+0

In seguito a ciò, sono riuscito a riscrivere 'Mod' usando il livello di tipo' If', che è stato compilato correttamente. Tuttavia, qualsiasi tentativo di ridurre un termine del modulo 'Modm n 'ha comportato un'eccezione di overflow dello stack. Modificare l'opzione _-freduction-depth_ mi ha mostrato che GHC stava dando priorità all'espansione della parte 'm-n' dell'espressione, senza rendersi conto che questo potrebbe non essere mai possibile. Dovrò cercare ulteriormente nell'estensione _DataKinds_ per capire meglio il comportamento. –

risposta

1

Non una risposta (non credo che ce ne sia ancora uno possibile), ma a beneficio di altre persone (come me) che tentano di rintracciare i passaggi OP nei commenti. Il seguente compila, ma usandolo rapidamente risulta un overflow dello stack.

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-} 
import GHC.TypeLits 
import Data.Type.Bool 

type family Mod (m :: Nat) (n :: Nat) :: Nat where 
    Mod m n = If (n <=? m) (Mod (m - n) n) m 

La ragione è che If sé è solo un tipo di famiglia regolare e il comportamento di tipo-famiglie è quello di iniziare espandendo i loro argomenti di tipo (desiderosi in un certo senso) prima di usare quelli del lato destro. Lo sfortunato risultato in questo caso è che Mod (m - n) n viene espanso anche se n <=? m è falso, quindi lo stack overflow.

Per esattamente la stessa ragione, gli operatori logici in Data.Type.Bool non cortocircuitare. Dato

type family Bottom :: Bool where Bottom = Bottom 

Possiamo vedere che False && Bottom e True || Bottom entrambi appendere.

EDIT

Nel caso in cui il PO è solo interessato a una famiglia tipo con il comportamento desiderato (e non solo il problema più generale di avere guardie in famiglie tipo) ci è un modo per esprimere Mod in un modo che termina:

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-} 
import GHC.TypeLits 

type Mod m n = Mod1 m n 0 m 

type family Mod1 (m :: Nat) (n :: Nat) (c :: Nat) (acc :: Nat) :: Nat where 
    Mod1 m n n acc = Mod1 m n 0 m 
    Mod1 0 n c acc = acc 
    Mod1 m n c acc = Mod1 (m - 1) n (c + 1) acc 
Problemi correlati