Created
November 7, 2020 15:22
-
-
Save Russoul/a3a5b6d1a2b841404be598867b022a79 to your computer and use it in GitHub Desktop.
Type-safe foreign values in Idris 2
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -- NOT A SELF-SUSTAINED EXAMPLE, WON'T RUN ON ITS OWN. | |
| ||| Any Lua value marked with a label, basically we assign a type to it. | |
| export | |
| data Typed : (label : a) -> Type where [external] | |
| ||| A proof that the given typed value is a table with an assessible key `field` holding a value of type `return` | |
| ||| Users can't normally build this proof term. | |
| export | |
| data ReadableField : (typed : Typed label) -> (field : String) -> (return : ty) -> Type where | |
| [noHints] -- The search engine shouldn't be able to directly construct a proof. | |
| MkReadableField : ReadableField typed field ty | |
| namespace ReadableField | |
| public export -- TODO preprocessor syntax to get rid of nested `function` syntax | |
| %foreign "function(_) return function (_) return function(_) return function(_) return function(table) return function(key) return table[key] end end end end" | |
| prim__getField : (typed : Typed label) -> (key : String) -> (0 readable : ReadableField typed key ty) => ty | |
| data Ty : Type where | |
| export | |
| %hint -- runtime irrelevant proof that any value of type `Typed Ty` is a readable dictionary with concrete keys | |
| -- and return values. | |
| 0 tyGuarantees : (typed : Typed Ty) -> HVect [ReadableField typed "test" String, ReadableField typed "ok" Int] | |
| -- Make the search engine do boring mechanical labor for us. | |
| -- The hint function has to return a concrete (non-generic) type because of the current Idris limitation. | |
| %hint | |
| readableHints : {typed : Typed label} -> (hv : HVect tyes) -> Elem (ReadableField typed field ty) tyes -> ReadableField typed field ty | |
| readableHints hv _ = get hv | |
| -- Just for testing purposes | |
| %foreign "TEST" | |
| someFunc : PrimIO (Typed Ty) | |
| testMeOk : IO Int | |
| testMeOk = do typed <- fromPrim someFunc | |
| let f = prim__getField typed "ok" | |
| pure f | |
| testMeNotOk : IO Int | |
| testMeNotOk = do typed <- fromPrim someFunc | |
| let f = prim__getField typed "ok1" | |
| pure f | |
| -- Error: While processing right hand side of testMeNotOk. Can't find an implementation for ReadableField typed "ok1" Int. | |
| -- /Users/russoul/my-stuff/projects/Idris2-Nvim/src/System/FFI/Lua.idr:66:26--66:52 | |
| -- | | |
| -- 66 | let f = prim__getField typed "ok1" | |
| -- | ^^^^^^^^^^^^^^^^^^^^^^^^^^ | |
| testMeNotOk' : IO String | |
| testMeNotOk' = do typed <- fromPrim someFunc | |
| let f = prim__getField typed "ok" | |
| pure f | |
| -- Error: While processing right hand side of testMeNotOk'. Can't find an implementation for ReadableField typed "ok" String. | |
| -- /Users/russoul/my-stuff/projects/Idris2-Nvim/src/System/FFI/Lua.idr:71:27--71:52 | |
| -- | | |
| -- 71 | let f = prim__getField typed "ok" | |
| -- | ^^^^^^^^^^^^^^^^^^^^^^^^^ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment