GitLocker: The Coding Marketplace

Description:

idrispython 0.25

idris-cam
Finally, we reached dependent types in Python community.

Install
pip install idris-python

Usage

Command: Idris-Python

Command: Run-Cam

## Example
Quite verbose for the lack of encapsulations, not a good example but I’m so busy..
Following example just revealed that I’ve alredy implmented such a big task.
module Main
import Cam.FFI
import Cam.IO
import Cam.Data.Collections
import Cam.Data.FCollections
import Cam.Data.Compat
import Data.Vect
import Data.HVect

%access export

main : IO ()
main = do
putStrLn $ show vect
sklearn <- camImport $ TheModule "sklearn.datasets"
load_iris <- camImportFrom sklearn "load_iris"
iris <- unsafeCall load_iris $ zero_ary
data' <- getattr iris "data"
tag <- getattr iris "target"
rfc <- let ensemble = camImport $ TheModule "sklearn.ensemble" in
camImportFrom !ensemble "RandomForestClassifier"
clf <- unsafeCall rfc zero_ary
fit <- getattr clf "fit"
unsafeCall fit . unsafe $ the (FList _) [data', tag]
score <- getattr clf "score"
value <- unsafeCall score . unsafe $ the (FList _) [data', tag] -- overfit
println value
where
vect : HVect [Int]
vect = the (HVect _) [1]

zero_ary : Unsafe
zero_ary = unsafe $ the (FList Unsafe) $ []

getattr' : IO Unsafe
getattr' = do
b <- camImport $ TheModule "builtins"
camImportFrom b "getattr"

getattr : Unsafe -> String -> IO Unsafe
getattr obj s =
let s = unsafe . the (Boxed String) $ s in
let args = unsafe . the (FHVect [_, _]) $ [obj, toText s] in
unsafeCall !getattr' args
You might got
[1]
0.99
If you run it as a file with command idris-python.