open-typerep: Open type representations and dynamic types

[ bsd3, dependent-types, library ] [ Propose Tags ]

This package uses Data Types à la Carte to provide open type representations and dynamic types/coercions for open type universes.

Example 1 (dynamic types):

type MyUniverse = IntType :+: BoolType

hlist :: [Dynamic MyUniverse]
hlist = [toDyn True, toDyn (1 :: Int)]
*Main> hlist

Note that if we were using Data.Dynamic, it would just print


Example 2 (dynamically typed addition):

addDyn :: (TypeEq ts ts, PWitness Num ts ts) => Dynamic ts -> Dynamic ts -> Maybe (Dynamic ts)
addDyn (Dyn ta a) (Dyn tb b) = do
    Dict <- typeEq ta tb
    Dict <- pwit pNum ta
    return (Dyn ta (a+b))

Data.Dynamic could only do this monomorphically, for one Num type at a time.


Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees


  • No Candidates
Versions [RSS] 0.1, 0.2, 0.3.1, 0.3.2, 0.3.3, 0.4, 0.5, 0.6, 0.6.1
Dependencies base (>=4 && <5), base-orphans, constraints (>=0.3), mtl (>=2.2.1), syntactic (>=3.1), tagged (>=0.4), template-haskell [details]
License BSD-3-Clause
Copyright Copyright (c) 2014-2016, Emil Axelsson
Author Emil Axelsson
Category Dependent Types
Home page
Bug tracker
Source repo head: git clone
Uploaded by EmilAxelsson at 2016-05-27T14:19:12Z
Reverse Dependencies 2 direct, 3 indirect [details]
Downloads 5501 total (36 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2016-05-27 [all 1 reports]