Skip to content

Instantly share code, notes, and snippets.

@divarvel
Created June 2, 2015 21:12
Show Gist options
  • Save divarvel/e25ee8d5758e3260cb89 to your computer and use it in GitHub Desktop.
Save divarvel/e25ee8d5758e3260cb89 to your computer and use it in GitHub Desktop.
Σpring
data Dependency : String -> Type -> Type
where MkDep : (name: String) -> a -> Dependency name a
DepWrapper : Type -> Type
DepWrapper t = (String ** Dependency _ t)
dep1 : Dependency "toto" Int
dep1 = MkDep "toto" 12
dep2 : Dependency "tutu" Int
dep2 = MkDep "tutu" 14
d1 : DepWrapper Int
d1 = ("toto" ** dep1)
d2 : DepWrapper Int
d2 = ("tutu" ** dep2)
deps : List (DepWrapper Int)
deps = [d1, d2]
hasName : String -> (DepWrapper Int) -> Bool
hasName s (n ** _) = s == n
findDep : String -> List (DepWrapper Int) -> Maybe (DepWrapper Int)
findDep s xs = find (hasName s) xs
myFunction : (DepWrapper Int) -> a
myFunction (_ ** (MkDep _ v)) = v
useDep : String -> Maybe Int
useDep depname =
let actualDep = findDep depname deps
actualRes = map myFunction actualDep
in actualRes
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment