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
Forse c'è una funzione di livello di tipo 'Se'? Penso di averlo visto da qualche parte, ma non sono un esperto di biblioteca ... – chi
Grazie, hai perfettamente ragione, "Se" esiste in [Data.Type.Bool] (https://hackage.haskell.org /package/base/docs/Data-Type-Bool.html). –
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. –