Tip aile örneklerindeki kısıtlamalar

Question

Haskell'deki tür aileleri araştırıyorum, tanımlayabileceğim tip düzeyindeki işlevlerin karmaşıklığını oluşturmaya çalışıyorum. Ben şöyle bir şey mod kapalı tip düzeyindeki sürümü tanımlamak istiyorum: İlk denklemde kısıt yasaktır olarak

{-# 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 

Ancak derleyici (GHC 7.10.2), bu reddeder. Değer seviyesindeki gardiyanlar tip seviyesine nasıl aktarılır? Bu şu anda Haskell'de mümkün mü?

Answer 1

Cevap değil (henüz bir tane bile mümkün olduğunu düşünmüyorum), fakat diğer kişilerin (benim gibi) faydaları için OP'leri yorumlarda tekrar gözden geçirmeye çalışıyorum. Aşağıdaki derlemeler, ancak bunu kullanarak hızlı bir şekilde yığın taşmasıyla sonuçlanır.

{-# 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 

nedeni If kendisi sıradan bir tip aile ve tip-ailelerin davranış sağ tarafta olanlar kullanmadan önce tip argümanları (bir anlamda istekli) genişleterek başlamaktır olmasıdır. Bu durumdaki talihsiz sonuç, n <=? m yanlış olsa bile, Mod (m - n) n'un genişletilmesi ve dolayısıyla yığının taşmasıdır.

Tam olarak aynı nedenle, Data.Type.Bool'daki mantıksal işleçler kısa devre yapmaz. Biz False && Bottom ve True || Bottom hem asmak görebilirsiniz

type family Bottom :: Bool where Bottom = Bottom 

Verilen.

DÜZENLEME

OP orada yılında Mod ifade etmenin bir yoludur olan gerekli davranışı ile bir tür aile içinde sadece ilgi (ve tip ailelerde korumaları sahip değil, sadece daha genel bir sorun) 'dir Ne olur ne

bir sonlandırma yolu:

{-# 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