singletons

singletons copied to clipboard

Singling Nat-indexed GADT with addition?

1

The following `genSingletons` application fails: ```haskell {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-}...

bgamari

Out-of-scope type variable when using `ScopedTypeVariables` in class method RHS

1

The following: ```hs {-# LANGUAGE GHC2021 #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -ddump-splices...

RyanGlScott

Consider allowing promotion and singling of all rank-1 types

5

Currently, `singletons-th` adopts a hard-line stance regarding quantifiers in type signatures. Namely, they must all appear at the top level in this order: ```hs forall tvb_1 ... tvb_m. ctx =>...

RyanGlScott

`Cabal-3.8` debuts a new [`code-generators`](https://github.com/haskell/cabal/pull/7688) feature that can be used to generate modules when preprocessing a test suite and include them as part of building the test suite. One of...

RyanGlScott

Split out `singletons-base` test suite into its own package

7

Before I explain why I want to do this, let me first make some observations about `singletons-base`'s minimum GHC requirements. Historically speaking, `singletons-base` has always been tied to a particular...

RyanGlScott

Knowing what is (and isn't) defunctionalized can be confusing

7

While pondering the questions in https://github.com/goldfirere/singletons/pull/427#discussion_r361532779, I realized that trying to document the existing status quo regarding what language constructs are OK to defunctionalize is much, much trickier than I...

RyanGlScott

Figure out how to promote visible type application sensibly

4

There's currently this line in `Data.Singletons.Promote`: https://github.com/goldfirere/singletons/blob/fb5e0051591f4e30109713e237bc2f0957406a3b/src/Data/Singletons/Promote.hs#L762-L765 Darn, if only we had visible kind applications! But hey, we're getting just that in GHC 8.8! Surely this means that we can...

RyanGlScott

Add S combinator i.e. ap for (->) a

4

The S combinator is occasionally useful for writing stuff in point-free style, if you're defining a type alias over a composition of the standard defunctionalisation symbols instead of writing your...

infinity0

Implementation details are needed for proofs

12

A proof about a function needs to have the implementation details of the function. In `singletons`, functions are type families, and type families must expose all their equations (AKA their...

howtonotwin

Singletonize functions that already use singletons

1

$(singletons [d| data Nat = Z | S Nat data Vec n a where VNil :: Vec 'Z a (:::) :: a -> Vec n a -> Vec ('S n)...

greatBigDot