`GHC.TypeLits` Öğesini Anlama

Question

Başı GHC uzantıları KindSignatures ve DataKinds etrafına sarmaya çalışıyorum. Data.Modular paketine bakınca

newtype i `Mod` (n :: Nat) = Mod i deriving (Eq, Ord) 

tür eşdeğer (yapıcı tip T sadece bir argüman alarak) bir C++ şablon <typename T, int N> ilan etmektir kabaca biliyoruz. Ancak, GHC.TypeLits paketine bakarak, neler olduğunu anlayamıyorum. Bu paket hakkında herhangi bir genel açıklama yararlı olacaktır.

• bir KnownNat sınıfı türünden tipi değişkeni ayıklamak izin gerekli fonksiyonu ile, mantıklı ama natVal ne yapar, ve: bu soru olsa konu dışı olarak işaretlendiğinde önce, burada bazı özel alt sorular proxy tip değişkeni nedir?
• someNatVal'u nerede kullanırsınız?
• Son olarak, SomeNat nedir - nasıl bir tür düzey numarası bilinmiyor? Derleme zamanında 'un olduğu bilinen bir düzey düzeyinin tamamı değil midir?

Answer 1

Bu soru oldukça geniştir - Sadece birkaç noktaya değineceğim.

proxy tip değişkeni, tür * -> * türünde bir tür değişkendir, yani türden bir tür yüklenicilerdir. Pragmatik olarak, 10 bir işleviniz varsa, örneğin, ör. Maybe Int, proxy = Maybe ve a = Int. [] Char ([Char] olarak da yazılmıştır) değerlerini de geçirebilirsiniz. Ya da, daha yaygın Proxy herhangi bir çalışma zamanı bilgisini taşımayan bir veri türü yani

data Proxy a = Proxy 

olarak tanımlanan bir veri türüdür tip Proxy Int, bir değeri (bunun için tek bir değer yoktur!), Ancak hangi derleme zamanı bilgisi taşır (phantom tip değişkeni a).

N türünde, bir derleme zamanı doğal olan Nat türünün bir türüdür. Biz bir işlev

bar :: N -> ... 

yazabilir ama bu çağıran tip N bir değer oluşturmak için bize gerektirecektir - önemsizdir. N türünün amacı, yalnızca derleme zamanı bilgilerini taşımaktır ve çalışma zamanı değerleri gerçekten kullanmak istediğimiz şeyler değildir. Aslında, N, alt haricinde hiç değer içermeyebilir. Biz olabilir çağrı

bar (undefined :: N) 

ama bu tuhaf görünüyor. Bunu okuyarak, ilk argümanında bar'un tembel olduğunu ve onu kullanmaya çalışan sapmaya neden olmadığını fark etmeliyiz. Sorun şu ki, bar :: N -> ... tip imzası yanıltıcıdır: Bu durum, aslında durum böyle olmadığında, N türünün argümanının değerine bağlı olabileceğini iddia eder.Bunun yerine, niyet açıktır

baz :: Proxy N -> ... 

kullanırsanız - sadece tek çalışma zamanı değeri bunun için vardır: Proxy :: Proxy N. N değerinin sadece derleme zamanında mevcut olduğu eşit derecede açıktır.

Bazen yerine belirli Proxy N kullanmak yerine, kod hafifçe

aynı hedefe ulaşır

foo :: proxy N -> ... 

için genelleştirilmiş ancak izni de farklı Proxy türlerini edilir. (Kişisel olarak, bu genellemeden çok fazla heyecan duymuyorum.)

Soruna geri dön: natVal, bir derleme zamanını yalnızca doğal bir çalışma zamanı değerine dönüştüren bir işlevdir. Yani 'u Int'a dönüştürerek sadece sabit değerini döndürür.

Derleme zamanı doğallarını modellemek için türünde şablon argümanlarını kullandıysanız C++ şablonları ile benzerlik elde edebilirsiniz. Örneğin. Onların çalışma zamanı değerleri, sadece kendi derleme zamanı bilgisi hususlar önemsizdir:

template <typename N> struct S { using pred = N; }; 
struct Z {}; 

template <typename N> int natVal(); 
template <typename N> int natVal() { return 1 + natVal<typename N::pred>(); } 
template <>   int natVal<Z>() { return 0; } 

int main() { 
    cout << natVal<S<S<Z>>>() << endl; // outputs 2 
    return 0; 
} 

Sadece S ve Z için hiçbir kamu kurucunun var davranırlar.