singletons

singletons copied to clipboard

Promote datatypes with arrows, among others

4

In thinking about #78, I realized that fixing that bug opens up a whole new possibility for promotion. Say a user wants to promote ``` data NatPred = MkNP (Nat...

goldfirere

Singletons of singletons

7

Can you single a singleton? Currently the answer is "no", since there's no `Sing` instances for `Sing`s. But should there be? Recently, I found myself wanting something like this when...

RyanGlScott

Singletons for Data.Functor.Product.Product?

5

This seems to be left out of the Prelude stuff, but I'm also unable to run `genSingletons` on this type: ```haskell genSingletons [''Data.Functor.Product.Product] ``` Produces ``` • Expected kind ‘*...

ocharles

Promote GADTs

38

Given inductively defined naturals `data N = Z | S N` we can define finite sets as follows: ``` haskell data Fin :: N -> Type where FZ :: Fin...

int-index

Terrible performance with singletonized maps

4

Just for fun, I decided to try porting `Data.Map` to `singletons`. I know, that's crazy. [Here's the code](https://gist.github.com/treeowl/c35362c7a7874a3c2b5643544639f1bb). It takes a while to compile that, but that doesn't bother me....

treeowl

Singling partiality in `do`-notation is troublesome

1

Even with https://github.com/goldfirere/th-desugar/pull/82, I'm not sure that we can properly single partial pattern matches in `do`-notation. For example, consider: ```haskell f :: [()] f = do Just () >= \arg...

RyanGlScott

Compile times with large sums

2

I have a data type with around 80 data constructors and derived instances for Eq,Ord,Bounded, and Enum. With ghc-7.10 and singletons-2.1, this compiled in somewhere near 15 seconds. With GHC8...

andrewthad

Figure out how match flattening affects us

6

In the `master` branch, all pattern-matches are "flattened" before further processing. This is done from `scLetDec` in `squashWildcards`, called in `singTopLevelDecs`. This is a drastic change, meaning that no patterns...

goldfirere

Compile regression with Singletons-2.0

6

The following code compiled with singletons-1.0 ``` {-# LANGUAGE DataKinds, GADTs, KindSignatures, PolyKinds, ScopedTypeVariables, TemplateHaskell, TypeFamilies, UndecidableInstances #-} module SingTest where import Data.Singletons.Prelude import Data.Singletons.TH import Data.Type.Natural ( Bool Z

crockeea

Export numeric functions that are in Prelude

4

Things like `even`, `(^)`, etc. See the export list of `Prelude`. Make sure to move the definition of `(:^)` from TypeLits when this is done.

goldfirere