Stack Overflow
Stack Overflow

Questions tagged [data-kinds]

For Haskell questions about involving the `-XDataKinds` extension in GHC. With -XDataKinds, GHC automatically promotes every suitable datatype to be a kind, and its (value) constructors to be type constructors.

155 questions
78
votes
2 answers

What is the DataKinds extension of Haskell?

I am trying to find an explanation of the DataKinds extension that will make sense to me having come from only having read Learn You a Haskell. Is there a standard source that will make sense to me with what little I've learned? Edit: For example…
user782220
  • 10,677
  • 21
  • 72
  • 135
36
votes
1 answer

What are all the mechanisms used to enable Servant's type-based API?

I'm very puzzled by how Servant is able to achieve the magic that it does using typing. The example on the web site already puzzles me greatly: type MyAPI = "date" :> Get '[JSON] Date :<|> "time" :> Capture "tz" Timezone :> Get '[JSON]…
user1002430
19
votes
1 answer

Can I provide the type-checker with proofs about inductive naturals in GHC 7.6?

GHC 7.6.1 comes with new features for programming at the type level, including datatype promotion. Taking the example about type-level naturals and vectors from there, I'd like to be able to write functions on vectors that rely on basic laws of…
Ganesh Sittampalam
  • 28,821
  • 4
  • 79
  • 98
17
votes
1 answer

Kind Demotion (as opposed to Kind Promotion)

The DataKinds extension promotes "values" (i.e. constructors) into types. For example True and False become distinct types of kind Bool. What I'd like to do is the opposite, i.e. demote types into values. A function with this signature would be…
Clinton
  • 22,361
  • 15
  • 67
  • 163
14
votes
1 answer

Haskell pattern matching on GADTs with Data Kinds

I have found that I really like combining GADTs with Data Kinds, as it gives me further type safety than before (for most uses, almost as good as Coq, Agda et al.). Sadly, pattern matching fails on the simplest of examples, and I could think of no…
Ramon Snir
  • 7,520
  • 3
  • 43
  • 61
13
votes
1 answer

How do you formulate n-ary product and sum types in this typed lambda calculus universe?

Here is the code where I'm having an issue: {-# LANGUAGE GADTs, LANGUAGE DataKinds #-} -- * Universe of Terms * -- type Id = String data Term a where Var :: Id -> Term a Lam :: Id -> Type -> Term b -> Term (a :-> b) App :: Term (a…
xiaolingxiao
  • 4,793
  • 5
  • 41
  • 88
13
votes
2 answers

Motivation for limitation on data kind promotion

Could anyone explain or guess the motivation behind the limit on data type promotion discussed in section 7.9.2 of the GHC user guide? The following restrictions apply to promotion: We only promote datatypes whose kinds are of the form * -> ... ->…
Doug McClean
  • 14,265
  • 6
  • 48
  • 70
12
votes
2 answers

Why does :k [False] result in an error in GHCI?

I'm confused about the error that I received at the end of the session below: $ ghci GHCi, version 7.10.2: http://www.haskell.org/ghc/ :? for help Ok, modules loaded: Main. *Main> :set -XDataKinds *Main> :t [False, True] [False, True] ::…
user1002430
12
votes
1 answer

Understanding the casts involved in patterns matching a datatype that is indexed over a user defined kind

So, I was playing around with DataKinds and TypeFamilies in Haskell and started to look at the Core GHC generated. Here is a little TestCase to motivate my question: {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DataKinds #-} {-#…
raichoo
  • 2,557
  • 21
  • 28
11
votes
2 answers

Is there a reason we can't populate types with DataKinds?

With DataKinds, a definition like data KFoo = TFoo introduces the kind KFoo :: BOX and the type TFoo :: KFoo. Why can't I then go on to define data TFoo = CFoo such that CFoo :: TFoo, TFoo :: KFoo, KFoo :: BOX? Do all constructors need to belong…
Dan
  • 12,409
  • 3
  • 50
  • 87
11
votes
1 answer

Implementing a zipper for length-indexed lists

I'm trying to implement a kind of zipper for length-indexed lists which would return each item of the list paired with a list where that element is removed. E.g. for ordinary lists: zipper :: [a] -> [(a, [a])] zipper = go [] where go _ [] …
shang
  • 24,642
  • 3
  • 58
  • 86
10
votes
0 answers

Is there any way to convince GHC that this (injective) type family is injective?

Messing around with GHC's DataKinds, I tried implementing type-level binary nats. They're simple enough to implement, but if I want them to be useful in common cases, then GHC needs to believe that the Succ type family is injective (so that type…
So8res
  • 9,856
  • 9
  • 56
  • 86
10
votes
1 answer

Haskell version of yin-yang puzzle : Kind incompatibility error

I want to implement the yin-yang puzzle in Haskell. Here is my attempt (unsucceful): -- The data type in use is recursive, so we must have a newtype defined newtype Cl m = Cl { goOn :: MonadCont m => Cl m -> m (Cl m) } yinyang :: (MonadIO m,…
Earth Engine
  • 10,048
  • 5
  • 48
  • 78
9
votes
2 answers

Singletons in Heterogenous Lists

I'd like to write a function which analyzes a heterogenous list. For sake of argument, let's have the following data Rec rs where Nil :: Rec '[] Cons :: ty -> Rec rs -> Rec ( '(name, ty) ': rs ) class Analyze name ty where analyze :: Proxy…
J. Abrahamson
  • 72,246
  • 9
  • 135
  • 180
9
votes
2 answers

Constructor that lifts (via DataKinds) to * -> A

Given an ADT like data K = A | B Bool the DataKinds extension allows us to lift it into kinds and types/type constructors K :: BOX 'A :: K 'B :: 'Bool -> K Is there a way to add a constructor to K that lifts to the type constructor 'C :: * -> K ?
Cactus
  • 27,075
  • 9
  • 69
  • 149
1
2 3
…
10 11