Kullanıcı tanımlı bir tür

Question

üzerinden endekslenen bir veri türü ile eşleşen kalıplarda yer alan kalıpları anlamak için, Haskell'de DataKinds ve TypeFamilies ile oynuyordum ve oluşturulan Core GHC'ye bakmaya başladım. İşte

sorumu motive etmek biraz TestCase geçerli:

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE KindSignatures #-} 

module TestCase where 

data Ty = TyBool | TyInt 

type family InterpTy (t :: Ty) :: * 
type instance InterpTy TyBool = Bool 
type instance InterpTy TyInt = Int 

data Expr (a :: Ty) where 
    I :: Int -> Expr TyInt 
    B :: Bool -> Expr TyBool 

eval :: Expr a -> InterpTy a 
eval (I i) = i 
eval (B b) = b 

en

TestCase.eval = 
    \ (@ (a_aKM :: TestCase.Ty)) (ds_dL3 :: TestCase.Expr a_aKM) -> 
    case ds_dL3 of _ [Occ=Dead] { 
     TestCase.I dt_dLh i_as6 -> 
     i_as6 
     `cast` (Sub (Sym TestCase.TFCo:R:InterpTyTyInt[0]) 
       ; (TestCase.InterpTy (Sym dt_dLh))_R 
       :: GHC.Types.Int ~# TestCase.InterpTy a_aKM); 
     TestCase.B dt_dLc b_as7 -> 
     b_as7 
     `cast` (Sub (Sym TestCase.TFCo:R:InterpTyTyBool[0]) 
       ; (TestCase.InterpTy (Sym dt_dLc))_R 
       :: GHC.Types.Bool ~# TestCase.InterpTy a_aKM) 
    } 

Açıkçası hakkında bilgi taşımanıza gerek eval fonksiyon için oluşturulan Çekirdek bir göz atalım neyi a belirli bir dalda olabilir. Ben TypeFamilies bir Datakind üzerinde indeksleme yoktur ve kullanmak ister ise dökme anlamak için çok daha kolaydır.

(Sub (Sym TestCase.TFCo:R:InterpTyTyInt[0]) 
     ; (TestCase.InterpTy (Sym dt_dLh))_R 
     :: GHC.Types.Int ~# TestCase.InterpTy a_aKM); 

ikinci satır gerçekten karıştırır şudur:

Main.eval = 
    \ (@ a_a1hg) (ds_d1sQ :: Main.Simpl a_a1hg) -> 
    case ds_d1sQ of _ [Occ=Dead] { 
     Main.I' dt_d1to i_aFa -> 
     i_aFa 
     `cast` (Sub (Sym dt_d1to) :: GHC.Integer.Type.Integer ~# a_a1hg); 
     Main.B' dt_d1tk b_aFb -> 
     b_aFb `cast` (Sub (Sym dt_d1tk) :: GHC.Types.Bool ~# a_a1hg) 
    } 

Gayet iyi anlayabiliyorum Bu ne TypeFamilies örnekte beni rahatsız bu parçasıdır:

Böyle bir şey olurdu ben mi. Burada yapılan noktalı virgül nedir? Burası biraz bozuk görünüyor mu yoksa bir şey mi özlüyorum?

Saygılarımızla Ben bu kadar okuyabilen bir yer var mı

raichoo

Answer 1

noktalı virgül baskılara dayanamayarak geçişlilik sözdizimi şöyledir, (eğer tavsiye eğer ben memnuniyetle kağıtları almak).

Sistem FC ile ilgili (Eylül 2014 itibariyle) son kağıt bu kağıt, Şekil 3 de baskılara sözdizimini bakınız özellikle

ICFP 2014 den "Safe Zero-Cost Coercions in Haskell" olup. "γ₁; γ₂", zorlayıcı geçişliliktir. "; Γ₂ γ₁" Bir zorlama tanık τ₁ ~ τ₃ olan γ₁ "τ₁ ~ τ₂" ve γ₂ ~ τ₃ sonra τ₂ tanıklar bir zorlama olduğu tanıklar bir zorlama olursa. Eğer derleyici sağ tarafta gördüğü eval (I i) = i yazma örnekte

, tip Int bir değerdir, ve ne (işlevin dönüş türünden) ihtiyacı InterpTy a ait bir şeydir. Yani şimdi o Int ~ InterpTy a bir kanıt inşa etmek gerekiyor.

Gayri resmi olarak, (sağdan sola doğru okuma ve rolleri görmezden - hangi bağlantılı kağıdı ayrıntılar için bkz):

1. biz "a ~ Int"
(yani dt_dLh var) olduğunu öğrenmek GADT desen maçı yapıyor itibaren
2. yüzden "Int ~ a" almak için, ona Sym geçerlidir.
3. Sonra beste Sonra
4. (/ bu/kongrüansının bir örneğidir) "InterpTy Int ~ InterpTy a" almak için InterpTy aileyi geçerli olduğunu geçişli ile "Sym InterpTyTyInt" (ki bu devletler aksiyomun çevrilmiş versiyonu olduğu "InterpTy TyInt ~ Int") Biz sonra biz zorlama almak için: "Int ~ InterpTy a"