हास्केल

Question

में विफलता के साथ बस लैम्ब्डा कैलकुस टाइप किया गया है, मैं हास्केल के लिए एक नवागंतुक हूं, इसलिए क्षमा करें यदि यह प्रश्न बहुत अधिक समझ में नहीं आता है।

मैं इस तरह से हास्केल में बस टाइप किया लैम्ब्डा भाव लागू करने के लिए कि जब मैं गलत प्रकार का एक और करने के लिए एक अभिव्यक्ति लागू करने के लिए प्रयास करते हैं, परिणाम एक प्रकार की त्रुटि नहीं है, बल्कि कुछ सेट में सक्षम होना चाहते मूल्य, उदाहरण के लिए कुछ भी तो नहीं। सबसे पहले मैंने सोचा कि शायद मोनड का उपयोग सही दृष्टिकोण होगा, लेकिन मैं कुछ भी काम नहीं कर पा रहा हूं। मुझे आश्चर्य हुआ कि, अगर कोई है, तो ऐसा करने का सही तरीका होगा।

समस्या का संदर्भ, यदि यह मदद करता है, तो एक ऐसी परियोजना है जिसे मैं काम कर रहा हूं जिस पर वाक्य में शब्दों में पीओएस (भाषण का हिस्सा) टैग असाइन किया जाता है। मेरे टैग सेट के लिए, मैं Categorial व्याकरण प्रकार का उपयोग कर रहा हूँ; इन्हें (e -> s) या (e -> (e -> s)) जैसे लैम्ब्डा अभिव्यक्तियों को टाइप किया गया है, जहां e और s क्रमशः संज्ञाओं और वाक्यों के प्रकार हैं। तो उदाहरण के लिए, kill में (e -> (e -> s)) है - इसमें दो संज्ञा वाक्यांश होते हैं और एक वाक्य देता है। मैं एक ऐसा फ़ंक्शन लिखना चाहता हूं जो इस प्रकार की वस्तुओं की एक सूची लेता है, और यह पता लगाता है कि s के किसी ऑब्जेक्ट तक पहुंचने के लिए उन्हें गठबंधन करने का कोई तरीका है या नहीं। बेशक, यह वैसे भी है जो हास्केल का प्रकार चेकर वैसे भी करता है, इसलिए प्रत्येक शब्द को उचित प्रकार की लैम्ब्डा अभिव्यक्ति असाइन करना सरल होना चाहिए, और हास्केल को बाकी करने दें। समस्या यह है कि, यदि s तक नहीं पहुंचा जा सकता है, तो हास्केल के प्रकार चेकर स्वाभाविक रूप से प्रोग्राम को चलने से रोकता है।

Answer 1

सुंदर मानक सामान। बस एक टाइप-चेकर लिखें, और टाइपकेक करते समय केवल उस शब्द का मूल्यांकन करें। evalMay यह करता है। आप निश्चित रूप से स्थिरांक और आधार प्रकारों के सेट को समृद्ध कर सकते हैं; मैंने सादगी के लिए प्रत्येक में से एक का उपयोग किया।

import Control.Applicative ((<$), (<$>)) 
import Control.Monad (guard) 
import Safe (atMay) 

data Type 
    = Base 
    | Arrow Type Type 
    deriving (Eq, Ord, Read, Show) 

data Term 
    = Const 
    | Var Int -- deBruijn indexing; the nearest enclosing lambda binds Var 0 
    | Lam Type Term 
    | App Term Term 
    deriving (Eq, Ord, Read, Show) 

check :: [Type] -> Term -> Maybe Type 
check env Const = return Base 
check env (Var v) = atMay env v 
check env (Lam ty tm) = Arrow ty <$> check (ty:env) tm 
check env (App tm tm') = do 
    Arrow i o <- check env tm 
    i' <- check env tm' 
    guard (i == i') 
    return o 

eval :: Term -> Term 
eval (App tm tm') = case eval tm of 
    Lam _ body -> eval (subst 0 tm' body) 
eval v = v 

subst :: Int -> Term -> Term -> Term 
subst n tm Const = Const 
subst n tm (Var m) = case compare m n of 
    LT -> Var m 
    EQ -> tm 
    GT -> Var (m-1) 
subst n tm (Lam ty body) = Lam ty (subst (n+1) tm body) 
subst n tm (App tm' tm'') = App (subst n tm tm') (subst n tm tm'') 

evalMay :: Term -> Maybe Term 
evalMay tm = eval tm <$ check [] tm 

Answer 2

मैं एक अलग दृष्टिकोण के साथ @Daniel वैगनर के उत्कृष्ट जवाब का विस्तार करना चाहते हैं: (यदि वहाँ एक है), एक मान्य प्रकार लौटने typechecking के बजाय एक टाइप किया अभिव्यक्ति है कि तो गारंटी है कि हम इसे मूल्यांकन कर सकते हैं वापसी (चूंकि बस टाइप किए गए लैम्ब्डा कैलकुस दृढ़ता से सामान्यीकृत होते हैं)। मूल विचार यह है check ctx t e रिटर्न Just (ctx |- e :: t)e iff कुछ संदर्भ ctx में t में टाइप किया जा सकता है, और फिर कुछ टाइप किया अभिव्यक्ति ctx |- e :: t दिया है हम सही प्रकार से कुछ Env ironment में यह मूल्यांकन कर सकते हैं।

कार्यान्वयन

मैं एकमात्र का उपयोग किया जाएगा check :: (ctx :: [Type]) -> (a :: Type) -> Term -> Maybe (TTerm ctx a) की पाई प्रकार, हम हर GHC विस्तार और पानी के नल को चालू करने की आवश्यकता होगी, जिसका मतलब है अनुकरण करने के लिए:

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-} 
{-# LANGUAGE TemplateHaskell #-} -- sigh... 

import Data.Singletons.Prelude 
import Data.Singletons.TH 
import Data.Type.Equality 

पहली बिट है untyped प्रतिनिधित्व, सीधे @Daniel वैगनर के जवाब से:

data Type = Base 
      | Arrow Type Type 
      deriving (Show, Eq) 

data Term = Const 
      | Var Int 
      | Lam Type Term 
      | App Term Term 
      deriving Show 

लेकिन हम भी इन प्रकार के अर्थ विज्ञान की व्याख्या से दे देंगे Base() के रूप में और Arrow t1 t2 रूप t1 -> t2:

type family Interp (t :: Type) where 
    Interp Base =() 
    Interp (Arrow t1 t2) = Interp t1 -> Interp t2 

de Bruijn विषय के साथ रखने के लिए, संदर्भों प्रकार की सूची है, और चर संदर्भ के सूचकांकों हैं। एक संदर्भ प्रकार के वातावरण को देखते हुए, हम मूल्य प्राप्त करने के लिए एक चर सूचकांक देख सकते हैं। ध्यान दें कि lookupVar कुल कार्य है।

data VarIdx (ts :: [Type]) (a :: Type) where 
    Here :: VarIdx (a ': ts) a 
    There :: VarIdx ts a -> VarIdx (b ': ts) a 

data Env (ts :: [Type]) where 
    Nil :: Env '[] 
    Cons :: Interp a -> Env ts -> Env (a ': ts) 

lookupVar :: VarIdx ts a -> Env ts -> Interp a 
lookupVar Here  (Cons x _) = x 
lookupVar (There v) (Cons _ xs) = lookupVar v xs 

ठीक है हमारे पास वास्तव में कुछ कोड लिखने के लिए सभी बुनियादी ढांचे हैं। अब तक तो अच्छा

data TTerm (ctx :: [Type]) (a :: Type) where 
    TConst :: TTerm ctx Base 
    TVar :: VarIdx ctx a -> TTerm ctx a 
    TLam :: TTerm (a ': ctx) b -> TTerm ctx (Arrow a b) 
    TApp :: TTerm ctx (Arrow a b) -> TTerm ctx a -> TTerm ctx b 

eval :: Env ctx -> TTerm ctx a -> Interp a 
eval env TConst =() 
eval env (TVar v) = lookupVar v env 
eval env (TLam lam) = \x -> eval (Cons x env) lam 
eval env (TApp f e) = eval env f $ eval env e 

: सबसे पहले, चलो एक साथ एक (! कुल) मूल्यांकनकर्ता के साथ, Term के द्वारा लिखा गया प्रतिनिधित्व परिभाषित करते हैं। eval अच्छा & कुल है क्योंकि इसका इनपुट केवल टाइप किए गए लैम्ब्डा कैलकुस के अच्छी तरह से टाइप की गई शर्तों का प्रतिनिधित्व कर सकता है। इसलिए @ डैनियल के मूल्यांकनकर्ता के काम का हिस्सा टाइप किए गए एक के प्रतिनिधित्व के परिवर्तन में किया जाना चाहिए।

infer के पीछे मूल विचार है कि प्रकार निष्कर्ष सफल होता है, यह रिटर्न Just $ TheTerm t e, जहां te के प्रकार का एक Sing LETON गवाह है।

$(genSingletons [''Type]) 
$(singDecideInstance ''Type) 

-- I wish I had sigma types... 
data SomeTerm (ctx :: [Type]) where 
    TheTerm :: Sing a -> TTerm ctx a -> SomeTerm ctx 

data SomeVar (ctx :: [Type]) where 
    TheVar :: Sing a -> VarIdx ctx a -> SomeVar ctx 

-- ... and pi ones as well 
infer :: Sing ctx -> Term -> Maybe (SomeTerm ctx) 
infer _ Const = return $ TheTerm SBase TConst 
infer ts (Var n) = do 
    TheVar t v <- inferVar ts n 
    return $ TheTerm t $ TVar v 
infer ts (App f e) = do 
    TheTerm t0 e' <- infer ts e 
    TheTerm (SArrow t0' t) f' <- infer ts f 
    Refl <- testEquality t0' t0 
    return $ TheTerm t $ TApp f' e' 
infer ts (Lam ty e) = case toSing ty of 
    SomeSing t0 -> do 
     TheTerm t e' <- infer (SCons t0 ts) e 
     return $ TheTerm (SArrow t0 t) $ TLam e' 

inferVar :: Sing ctx -> Int -> Maybe (SomeVar ctx) 
inferVar (SCons t _) 0 = return $ TheVar t Here 
inferVar (SCons _ ts) n = do 
    TheVar t v <- inferVar ts (n-1) 
    return $ TheVar t $ There v 
inferVar _ _ = Nothing 

उम्मीद है कि अंतिम चरण स्पष्ट है: के बाद से हम केवल एक दिया प्रकार पर एक अच्छी तरह से टाइप किया अवधि मूल्यांकन कर सकते हैं (के बाद से है कि क्या हमें अपने हास्केल एम्बेडिंग के प्रकार देता है), हम प्रकार check में प्रकार बारी infer खिलाडि़यों ing:

check :: Sing ctx -> Sing a -> Term -> Maybe (TTerm ctx a) 
check ctx t e = do 
    TheTerm t' e' <- infer ctx e 
    Refl <- testEquality t t' 
    return e' 

उदाहरण सत्र

के GHCi में हमारे कार्यों को कोशिश करते हैं:

λ» :set -XStandaloneDeriving -XGADTs 
λ» deriving instance Show (VarIdx ctx a) 
λ» deriving instance Show (TTerm ctx a) 

λ» let id = Lam Base (Var 0) -- \x -> x 
λ» check SNil (SBase `SArrow` SBase) id 
Just (TLam (TVar Here)) 

λ» let const = Lam Base $ Lam Base $ Var 1 -- \x y -> x 
λ» check SNil (SBase `SArrow` SBase) const 
Nothing -- Oops, wrong type 
λ» check SNil (SBase `SArrow` (SBase `SArrow` SBase)) const 
Just (TLam (TLam (TVar Here))) 

λ» :t eval Nil <$> check SNil (SBase `SArrow` (SBase `SArrow` SBase)) const 
eval Nil <$> check SNil (SBase `SArrow` (SBase `SArrow` SBase)) const 
    :: Maybe (() ->() ->()) 
-- Note that the `Maybe` there comes from `check`, not `eval`! 
λ» let Just const' = check SNil (SBase `SArrow` (SBase `SArrow` SBase)) const 
λ» :t eval Nil const' 
eval Nil const' ::() ->() ->() 
λ» eval Nil const'()() 
()