singletons
singletons copied to clipboard
goldfirere
Fake dependent types in Haskell using singletons
Currently, `singletons-th` always attempts to generate instance signatures for singled instance methods, even if the original instance code lacks instance signatures. For instance, `singletons-th` will take this code: ```hs instance...
As explained in [`Note [Promoted class methods and kind variable ordering]`](https://github.com/goldfirere/singletons/blob/aad81c85c515a71cfd771915bab7e79295fe82ef/singletons-th/src/Data/Singletons/TH/Promote.hs#L316-L357), `singletons-th` makes no effort to ensure that the kind of a promoted class method quantifies its kind variables in...
GHC recently landed [!9480](https://gitlab.haskell.org/ghc/ghc/-/merge_requests/9480), an implementation of [GHC proposal #425](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst). This introduces invisible `@k`-binders for type-level declarations, guarded behind the `TypeAbstractions` extension. For example: ``` data D @k @j (a...
GHC 9.10 introduces the ability to use [invisible type patterns](https://gitlab.haskell.org/ghc/ghc/-/merge_requests/11109). As such, examples like this can now be written: ```hs id :: a -> a id @t x = x...
There is a surprising amount of special-casing for the `error` and `undefined` functions during singling: https://github.com/goldfirere/singletons/blob/aad81c85c515a71cfd771915bab7e79295fe82ef/singletons-th/src/Data/Singletons/TH/Single.hs#L886-L890 https://github.com/goldfirere/singletons/blob/aad81c85c515a71cfd771915bab7e79295fe82ef/singletons-th/src/Data/Singletons/TH/Single.hs#L894-L901 https://github.com/goldfirere/singletons/blob/aad81c85c515a71cfd771915bab7e79295fe82ef/singletons-th/src/Data/Singletons/TH/Single.hs#L795-L807 I've read `Note [Why error is so special]`, but I'm still unclear...
GHC 9.10.1 [adds support for namespaces in fixity declarations](https://gitlab.haskell.org/ghc/ghc/-/merge_requests/12012), e.g., ```hs $(singletons [d| infixl 4 data `f` f :: a -> a -> a |]) ``` It would be nice...
Hi, @jul1u5 and I are trying to manually write a special singleton data type for gradually typed hasktorch. We'd like a generic singleton datatype, `SChecked a`, that makes it possible...
The following type family is often useful: ```haskell type LazyTake :: Nat -> [k] -> [k] type family LazyTake n xs where LazyTake 0 _ = '[] LazyTake n xs...
With singletons-3.0 and singletons-th-3.0, if I try to generate a singled data type with `TypeRep` as one of the fields, with `genSingletons`, for instance: ```haskell data MvType s where MvHsT...
Consider the program below. I think it's uncontroversial (although there's a possibility that I've misunderstood how `Apply` instances are supposed to be written). This is probably the simplest possible program...
Metadata
Owner
Metadata
Fake dependent types in Haskell using singletons