Skip to content

Instantly share code, notes, and snippets.

@xaviervia
Created April 5, 2017 19:42
Show Gist options
  • Save xaviervia/55b0f8fe479914b46e532d3166d83a5b to your computer and use it in GitHub Desktop.
Save xaviervia/55b0f8fe479914b46e532d3166d83a5b to your computer and use it in GitHub Desktop.
interface Parseable a where
parse : String -> a
data Name : Type where
MkName : String -> Name
Parseable Name where
parse = MkName
data A : Type -> Type where
MkA : Parseable a => (a -> a) -> A a
f : Name -> Name
read : String -> A t -> t
read s (MkA f) = parse s
@xaviervia
Copy link
Author

Using it:

*ArtificialConstraint> :let arg = MkA f
Holes: Main.f
*ArtificialConstraint> read "asdas" arg
MkName "asdas" : Name
Holes: Main.f

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment