thautwarm/idris-python

Successor project: https://github.com/thautwarm/Quick-Backend

idris-Python

Finally, we reached dependent types in Python side.

Requirements

• The Haskell Tool Stack
• Python 3.7+

P.S: For users of Python3.7-, you can make a PR to remove the usages of dataclass and from __future__ import annotations to support almost all Python versions, which I don't have time and motivations to deal with.

Install

Firstly you should clone Idris-Cam and install it:

git clone https://github.com/thautwarm/idris-cam/
cd idris-cam
stack build
stack install        # install idris-codegen-cam
stack install idris  # install idris
cd libs
idris --install cam.ipkg # install cam modules for idris

Then install idris-python,

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 too busy to work for this.

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.