Cách tạo các hàm được nhập ngẫu nhiên

Question

Tôi muốn tạo các hàm Haskell ngẫu nhiên theo lập trình và đánh giá chúng. Dường như với tôi rằng cách duy nhất để làm điều này là về cơ bản tạo mã Haskell theo chương trình và chạy nó bằng cách sử dụng API GHC hoặc một quá trình bên ngoài, trả về một chuỗi và phân tích nó trở lại thành kiểu dữ liệu Haskell. Điều này có đúng không?

Lý do của tôi là như sau. Các chức năng là đa hình vì vậy tôi không thể sử dụng Typeable. Quan trọng hơn, ngay cả khi tôi viết trình kiểm tra kiểu của riêng tôi và chú thích từng hàm với kiểu của nó, tôi không thể chứng minh cho trình biên dịch Haskell mà trình kiểm tra kiểu của tôi là đúng. Ví dụ, khi tôi lấy hai hàm ra khỏi một tập hợp hàm không đồng nhất và áp dụng một hàm khác, tôi cần cung cấp trình biên dịch với một đảm bảo rằng hàm tôi đang sử dụng để chọn các hàm này chỉ chọn các hàm với các kiểu tương ứng. Nhưng không có cách nào để làm điều này, phải không?

Answer 1

bình luận DarkOtter của đề cập QuickCheck của Arbitrary và CoArbitrary lớp học, mà chắc chắn là điều đầu tiên bạn nên thử. QuickCheck có trường hợp này:

instance (CoArbitrary a, Arbitrary b) => Arbitrary (a -> b) where ... 

Vì điều này xảy ra, hôm qua tôi đã đọc mã QuickCheck để hiểu cách thức hoạt động, vì vậy tôi có thể chia sẻ những gì tôi đã học được trong tâm trí. QuickCheck được xây dựng xung quanh một loại trông như thế này (và điều này sẽ không hoàn toàn giống nhau):

type Size = Int 

-- | A generator for random values of type @a@. 
newtype Gen a = 
    MkGen { -- | Generate a random @a@ using the given randomness source and 
      -- size. 
      unGen :: StdGen -> Size -> a 
      } 

class Arbitrary a where 
    arbitrary :: a -> Gen a 

Bí quyết đầu tiên là QuickCheck có một chức năng mà làm việc như thế này (và tôi đã không làm việc ra chính xác cách nó thực hiện):

-- | Use the given 'Int' to \"perturb\" the generator, i.e., to make a new 
-- generator that produces different pseudorandom results than the original. 
variant :: Int -> Gen a -> Gen a 

Sau đó, họ sử dụng để thực hiện các trường hợp khác nhau của CoArbitrary lớp này:

class CoArbitrary a where 
    -- | Use the given `a` to perturb some generator. 
    coarbitrary :: a -> Gen b -> Gen b 

-- Example instance: we just treat each 'Bool' value as an 'Int' to perturb with. 
instance CoArbitrary Bool where 
    coarbitrary False = variant 0 
    coarbitrary True = variant 1 

Bây giờ với những mảnh tại chỗ, chúng tôi muốn điều này:

instance (Coarbitrary a, Arbitrary b) => Arbitrary (a -> b) where 
    arbitrary = ... 

Tôi sẽ không viết ra thực hiện, nhưng ý tưởng là thế này:

1. Sử dụng CoArbitrary thể hiện của a và Arbitrary thể hiện của b chúng ta có thể thực hiện chức năng \a -> coarbitrary a arbitrary, trong đó có gõ a -> Gen b.
2. Hãy nhớ rằng Gen b là kiểu mới cho StdGen -> Size -> b, do đó, loại a -> Gen b là đẳng cấu để a -> StdGen -> Size -> b.
3. Chúng ta có thể viết một hàm nhỏ bất kỳ chức năng nào của loại thứ hai đó và chuyển thứ tự đối số xung quanh để trả về một hàm thuộc loại StdGen -> Size -> a -> b.
4. Loại sắp xếp lại này là đẳng cấu để Gen (a -> b), do đó, chúng tôi đóng gói chức năng sắp xếp lại thành một Gen và chúng tôi có bộ tạo hàm ngẫu nhiên!

Tôi khuyên bạn nên đọc nguồn QuickCheck để xem điều này cho chính mình. Khi bạn giải quyết điều đó, bạn sẽ chỉ chạy vào hai chi tiết bổ sung có thể làm chậm bạn xuống. Thứ nhất, lớp Haskell RandomGen có phương pháp này:

-- | The split operation allows one to obtain two distinct random generators. 
split :: RandomGen g => g -> (g, g) 

Thao tác này được sử dụng trong Monad dụ cho Gen, và là khá quan trọng. Một trong những thủ thuật ở đây là StdGen là một trình tạo số ngẫu nhiên giả ngẫu nhiên; cách hoạt động Gen (a -> b) là cho mỗi giá trị có thể của a chúng tôi làm nhiễu máy phát điện b, hãy sử dụng máy phát điện bị nhiễu loạn đó để tạo kết quả b, nhưng sau đó chúng tôi không bao giờ chuyển trạng thái của máy phát điện bị nhiễu loạn; về cơ bản, hàm a -> b được tạo ra là một đóng trên một hạt giả ngẫu nhiên, và mỗi lần chúng ta gọi nó là a để sử dụng cụ thể đó là a để xác định một hạt giống mới, và sau đó sử dụng nó để xác định một b phụ thuộc vào a và hạt giống ẩn.

Loại viết tắt Seed -> a -> b nhiều hay ít tổng kết những gì đang xảy ra — chức năng giả ngẫu nhiên là quy tắc tạo số b từ hạt giả ngẫu nhiên và a. Điều này sẽ không hoạt động với các trình tạo số ngẫu nhiên trạng thái bắt buộc.

Thứ hai: thay vì trực tiếp có chức năng (a -> StdGen -> Size -> b) -> StdGen -> Size -> a -> b như tôi đã mô tả ở trên, mã QuickCheck có promote :: Monad m => m (Gen a) -> Gen (m a), là sự tổng quát hóa điều đó với bất kỳ Monad nào. Khi m là phiên bản chức năng của Monad, promote trùng với (a -> Gen b) -> Gen (a -> b), vì vậy nó thực sự giống như tôi phác thảo ở trên.

Answer 2

Điều gì đó dọc theo những dòng này có đáp ứng nhu cầu của bạn không?

import Control.Monad.Random 

randomFunction :: (RandomGen r, Random a, Num a, Floating a) => Rand r (a -> a) 
randomFunction = do 
    (a:b:c:d:_) <- getRandoms 
    fromList [(\x -> a + b*x, 1), (\x -> a - c*x, 1), (\x -> sin (a*x), 1)] 
    -- Add more functions as needed 

main = do 
    let f = evalRand randomFunction (mkStdGen 1) :: Double -> Double 
    putStrLn . show $ f 7.3 

---

EDIT: xây dựng trên ý tưởng đó, chúng tôi có thể kết hợp chức năng mà có số lượng khác nhau và các loại thông số ... miễn là chúng ta phần nào áp dụng chúng để họ tất cả đều có loại kết quả tương tự .

import Control.Monad.Random 

type Value = (Int, Double, String) -- add more as needed 

type Function = Value -> String -- or whatever the result type is 

f1 :: Int -> Int -> (Int, a, b) -> Int 
f1 a b (x, _, _) = a*x + b 

f2 :: String -> (a, b, String) -> String 
f2 s (_, _, t) = s ++ t 

f3 :: Double -> (a, Double, b) -> Double 
f3 a (_, x, _) = sin (a*x) 

randomFunction :: RandomGen r => Rand r Function 
randomFunction = do 
    (a:b:c:d:_) <- getRandoms -- some integers 
    (w:x:y:z:_) <- getRandoms -- some floats 
    n <- getRandomR (0,100) 
    cs <- getRandoms -- some characters 
    let s = take n cs 
    fromList [(show . f1 a b, 1), (show . f2 s, 1), (show . f3 w, 1)] 
    -- Add more functions as needed 

main = do 
    f <- evalRandIO randomFunction :: IO Function 
    g <- evalRandIO randomFunction :: IO Function 
    h <- evalRandIO randomFunction :: IO Function 
    putStrLn . show $ f (3, 7.3, "hello") 
    putStrLn . show $ g (3, 7.3, "hello") 
    putStrLn . show $ h (3, 7.3, "hello") 

Answer 3

Cảm ơn các câu trả lời rất kỹ lưỡng ở trên! Không có câu trả lời nào, hoàn toàn làm những gì tôi đang tìm kiếm. Tôi theo dõi gợi ý của DarkOtter trong phần bình luận câu hỏi, và sử dụng unsafeCoerce tránh trình kiểm tra kiểu. Ý tưởng cơ bản là chúng ta tạo một GADT đóng gói các hàm Haskell với các kiểu của chúng; khi tôi muốn có một bộ sưu tập các hàm Haskell, trước hết tôi ép chúng thành các loại Any, sau đó tôi làm những gì tôi cần làm, ghép chúng lại với nhau một cách ngẫu nhiên. Khi tôi đi để đánh giá các chức năng mới, đầu tiên tôi ép chúng trở lại loại tôi muốn. Tất nhiên, điều này không an toàn; nếu trình kiểm tra loại của tôi sai hoặc tôi chú thích các hàm haskell có các loại không chính xác, thì tôi kết thúc với vô nghĩa.

Tôi đã dán mã tôi đã thử nghiệm điều này với bên dưới. Lưu ý rằng có hai mô-đun cục bộ được nhập Strappy.Type và Strappy.Utils. Đầu tiên là hệ thống kiểu được đề cập ở trên. Thứ hai mang đến những người trợ giúp cho các chương trình ngẫu nhiên.

Lưu ý: trong mã bên dưới, tôi đang sử dụng logic kết hợp làm ngôn ngữ cơ bản. Đó là lý do tại sao ngôn ngữ biểu thức của tôi chỉ có ứng dụng và không có biến hoặc trừu tượng lambda.

{-# Language GADTs, ScopedTypeVariables #-} 

import Prelude hiding (flip) 
import qualified Data.List as List 
import Unsafe.Coerce (unsafeCoerce) 
import GHC.Prim 
import Control.Monad 
import Control.Monad.State 
import Control.Monad.Trans 
import Control.Monad.Identity 
import Control.Monad.Random 

import Strappy.Type 
import Strappy.Utils (flip) 


-- | Helper for turning a Haskell type to Any. 
mkAny :: a -> Any 
mkAny x = unsafeCoerce x 


-- | Main data type. Holds primitive functions (Term), their 
-- application (App) and annotations. 
data Expr a where 
    Term :: {eName :: String, 
      eType :: Type, 
      eThing :: a} -> Expr a 
    App :: {eLeft :: (Expr (b -> a)), 
      eRight :: (Expr b), 
      eType :: Type}   -> Expr a 

-- | smart constructor for applications 
a <> b = App a b (fst . runIdentity . runTI $ typeOfApp a b) 

instance Show (Expr a) where 
    show Term{eName=s} = s 
    show App{eLeft=el, eRight=er} = "(" ++ show el ++ " " ++ show er ++ ")" 



-- | Return the resulting type of an application. Run's type 
-- unification. 
typeOfApp :: Monad m => Expr a -> Expr b -> TypeInference m Type 
typeOfApp e_left e_right 
    = do t <- newTVar Star 
     case mgu (eType e_left) (eType e_right ->- t) of 
      (Just sub) -> return $ toType (apply sub (eType e_left)) 
      Nothing -> error $ "typeOfApp: cannot unify " ++ 
         show e_left ++ ":: " ++ show (eType e_left) 
           ++ " with " ++ 
         show e_right ++ ":: " ++ show (eType e_right ->- t) 

eval :: Expr a -> a 
eval Term{eThing=f} = f 
eval App{eLeft=el, eRight=er} = (eval el) (eval er) 

filterExprsByType :: [Any] -> Type -> TypeInference [] Any 
filterExprsByType (e:es) t 
    = do et <- freshInst (eType (unsafeCoerce e :: Expr a)) 
     let e' = unsafeCoerce e :: Expr a 
     case mgu et t of 
      Just sub -> do let eOut = unsafeCoerce e'{eType = apply sub et} :: Any 
          return eOut `mplus` rest 
      Nothing -> rest 
     where rest = filterExprsByType es t 
filterExprsByType [] t = lift [] 


---------------------------------------------------------------------- 
-- Library of functions 

data Library = Library { probOfApp :: Double, --^probability of an expansion 
         libFunctions :: [Any] } 

cInt2Expr :: Int -> Expr Int 
-- | Convert numbers to expressions. 
cInt2Expr i = Term (show i) tInt i 


-- Some basic library entires. 
t = mkTVar 0     
t1 = mkTVar 1     
t2 = mkTVar 2     
t3 = mkTVar 3     

cI = Term "I" (t ->- t) id 
cS = Term "S" (((t2 ->- t1 ->- t) ->- (t2 ->- t1) ->- t2 ->- t)) $ \f g x -> (f x) (g x) 
cB = Term "B" ((t1 ->- t) ->- (t2 ->- t1) ->- t2 ->- t) $ \f g x -> f (g x) 
cC = Term "C" ((t2 ->- t1 ->- t2 ->- t) ->- t1 ->- t2 ->- t) $ \f g x -> (f x) g x 
cTimes :: Expr (Int -> Int -> Int) 
cTimes = Term "*" (tInt ->- tInt ->- tInt) (*) 
cPlus :: Expr (Int -> Int -> Int) 
cPlus = Term "+" (tInt ->- tInt ->- tInt) (+) 
cCons = Term ":" (t ->- TAp tList t ->- TAp tList t) (:) 
cAppend = Term "++" (TAp tList t ->- TAp tList t ->- TAp tList t) (++) 
cHead = Term "head" (TAp tList t ->- t) head 
cMap = Term "map" ((t ->- t1) ->- TAp tList t ->- TAp tList t1) map 
cEmpty = Term "[]" (TAp tList t) [] 
cSingle = Term "single" (t ->- TAp tList t) $ \x -> [x] 
cRep = Term "rep" (tInt ->- t ->- TAp tList t) $ \n x -> take n (repeat x) 
cFoldl = Term "foldl" ((t ->- t1 ->- t) ->- t ->- (TAp tList t1) ->- t) $ List.foldl' 
cNums = [cInt2Expr i | i <- [1..10]] 

-- A basic library 

exprs :: [Any] 
exprs = [mkAny cI, 
     mkAny cS, 
     mkAny cB, 
     mkAny cC, 
     mkAny cTimes, 
     mkAny cCons, 
     mkAny cEmpty, 
     mkAny cAppend, 
--   mkAny cHead, 
     mkAny cMap, 
     mkAny cFoldl, 
     mkAny cSingle, 
     mkAny cRep 
     ] 
     ++ map mkAny cNums 

library = Library 0.3 exprs 


-- | Initializing a TypeInference monad with a Library. We need to 
-- grab all type variables in the library and make sure that the type 
-- variable counter in the state of the TypeInference monad is greater 
-- that that counter. 
initializeTI :: Monad m => Library -> TypeInference m() 
initializeTI Library{libFunctions=es} = do put (i + 1) 
              return() 
    where go n (expr:rest) = let tvs = getTVars (unsafeCoerce expr :: Expr a) 
           getTVars expr = tv . eType $ expr 
           m = maximum $ map (readId . tyVarId) tvs 
          in if null tvs then 0 else go (max n m) rest 
      go n [] = n 
      i = go 0 es 


---------------------------------------------------------------------- 
---------------------------------------------------------------------- 
-- Main functions. 
sampleFromExprs :: (MonadPlus m, MonadRandom m) => 
        Library -> Type -> TypeInference m (Expr a) 
-- | Samples a combinator of type t from a stochastic grammar G. 
sampleFromExprs lib@Library{probOfApp=prApp, libFunctions=exprs} tp 
    = do initializeTI lib 
     tp' <- freshInst tp 
     sample tp' 
    where sample tp = do 
      shouldExpand <- flip prApp 
      case shouldExpand of 
       True -> do t <- newTVar Star 
         (e_left :: Expr (b -> a)) <- unsafeCoerce $ sample (t ->- tp) 
         (e_right :: Expr b) <- unsafeCoerce $ sample (fromType (eType e_left)) 
         return $ e_left <> e_right -- return application 
       False -> do let cs = map fst . runTI $ filterExprsByType exprs tp 
          guard (not . null $ cs) 
          i <- getRandomR (0, length cs - 1) 
          return $ unsafeCoerce (cs !! i) 

---------------------------------------------------------------------- 
---------------------------------------------------------------------- 

main = replicateM 100 $ 
     do let out = runTI $ do sampleFromExprs library (TAp tList tInt) 
      x <- catch (liftM (Just . fst) out) 
        (\_ -> putStrLn "error" >> return Nothing)      
      case x of 
      Just y -> putStrLn $ show x ++ " " ++ show (unsafeCoerce (eval y) :: [Int]) 
      Nothing -> putStrLn ""