[commit: base] master: Add code to convert from representation types, to existentially quantified singletons. (f7fb908)

Iavor Diatchki diatchki at galois.com
Thu May 30 18:52:50 CEST 2013


Repository : ssh://darcs.haskell.org//srv/darcs/packages/base

On branch  : master

https://github.com/ghc/packages-base/commit/f7fb908ad963f7180c30b55fba57a858b0391de4

>---------------------------------------------------------------

commit f7fb908ad963f7180c30b55fba57a858b0391de4
Author: Iavor S. Diatchki <diatchki at Perun.(none)>
Date:   Mon May 27 14:44:59 2013 -0700

    Add code to convert from representation types, to existentially quantified singletons.
    
    The basic idea is like this:
    
    data SomeSing where SomeSing :: SingI n => Proxy n -> SomeSing
    
    toSing :: Integer -> Maybe SomeSing  -- Maybe, so that we rejetc -ve numbers
    
    The actual implementation is a bit more complicated because `SomeSing`
    is actually parameterized by a kind, so we really have something akin
    `SomeSing k`.  Also, `toSing` is a bit more general because, depending
    on the kind, the representation is different.  For example, we also
    support:
    
    toSing :: String -> Maybe (SomeSing (KindParam :: KindIs Symbol))
    
    
    This change relies on the primitive added to the compiler, which
    converts `Sing` values into `SingI` dictionaries.
    
    A nice benefit of this change is that, as far as I can see,
    we don't need  `unsafeSinNat` and friends, so I removed them.

 GHC/TypeLits.hs |  120 +++++++++++++++++++++++++++++++++++++++++++------------
 1 files changed, 94 insertions(+), 26 deletions(-)


Diff suppressed because of size. To see it, use:

    git show f7fb908ad963f7180c30b55fba57a858b0391de4



More information about the ghc-commits mailing list