data-kinds Questions

2

Solved

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 -XDataKi...
Dropsonde asked 5/11, 2015 at 20:56

1

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 :<|&g...
Hoiden asked 31/10, 2015 at 20:6

3

Solved

The following example is a boiled-down version of my real-life problem. It seems to be in some way similar to Retrieving information from DataKinds constrained existential types, but I could not qu...
Interwork asked 4/9, 2015 at 23:54

1

Solved

How does one define new computation over types of kind GHC.TypeLits.Nat? I am hoping to be able to define a type family type family WIDTH (n :: Nat) :: Nat such that WIDTH 0 ~ 0 and WIDTH (n+1) ...
Rozella asked 16/6, 2015 at 11:44

2

Solved

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 construc...
Mood asked 11/6, 2015 at 13:15

1

Solved

Disclaimer GADTs & DataKinds are unexplored territory for me, so some of the limitations and capabilities of them are unknown to me. The Question So I'm writing an AST for a JavaScript code ...
Norinenorita asked 7/2, 2015 at 23:25

2

Solved

Let's say I have a Currency type: data Currency = USD | EUR | YEN and a Money type that stores an int, and is parameterized by a given Currency (Currency is promoted to a kind with the DataKinds...
Sousaphone asked 2/2, 2015 at 18:11

1

Solved

I've been playing with -XDataKinds recently, and would like to take a promoted structure build with type families and pull it back down to the value level. I believe this is possible because the co...
Heartfelt asked 19/1, 2015 at 17:15

0

I've been toying around with -XDataKinds recently, and was wondering why Foo below won't be automatically promoted: {-# LANGUAGE GADTs , DataKinds , KindSignatures #-} import Data.HList data ...
Unbonnet asked 17/12, 2014 at 15:0

0

I'm using the genifunctors package to generate a functor instance for a type whose definition involves type families. The first module defines the data type itself: {-# LANGUAGE TypeFamilies #-} ...
Minoru asked 26/9, 2014 at 13:24

1

Solved

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 #-} {-# LA...
Balzer asked 19/9, 2014 at 12:42

2

Solved

I'm trying to derive a Typeable instance for tupled constraints. See the following code: {-# LANGUAGE ConstraintKinds, GADTs #-} {-# LANGUAGE DataKinds, PolyKinds, AutoDeriveTypeable #-} {-# LANG...
Chicanery asked 17/9, 2014 at 14:19

1

Solved

I found an interesting situation, when using data kinds with type families. The compiler's error message is No instance for (C (ID ())) arising from a use of W. It suggests that a type family appl...
Praedial asked 16/9, 2014 at 16:32

2

Solved

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 ::...
Bosomed asked 26/6, 2014 at 20:27

1

Solved

If I have a type constrained by a finite DataKind {-# LANGUAGE DataKinds #-} data K = A | B data Ty (a :: K) = Ty { ... } and an existential type which forgets the exact choice of K in the typ...
Workhouse asked 24/6, 2014 at 13:25

2

Solved

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...
Assignment asked 13/12, 2013 at 3:36

2

Solved

Why is it harder to build values with datakinds, while it's relatively easy to pattern match with them? {-# LANGUAGE KindSignatures , GADTs , DataKinds , Rank2Types #-} data Nat = Zero | Suc...
Farthermost asked 4/5, 2014 at 0:39

1

Solved

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 -&gt...
Jeannettajeannette asked 20/1, 2014 at 15:58

2

Solved

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...
Guessrope asked 18/1, 2014 at 16:21

2

Solved

I've been reading on vinyl recently, which uses weird "list of kinds" kinda types. After reading a bit on kinds and vinyl, I've gotten somewhat of an intuitive understanding of them, and I've been ...
Number asked 26/11, 2013 at 21:51

1

Solved

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...
Toby asked 14/11, 2013 at 3:23

1

Solved

I'm having problems getting GHC to infer a type in a place where it should be obvious. Below is a complete snippet demonstrating the problem. {-# LANGUAGE DataKinds, ScopedTypeVariables, KindSigna...
Joselow asked 10/9, 2013 at 3:14

1

Solved

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] ...
Dorene asked 6/7, 2013 at 9:57

1

Solved

So let's say I wrote some type-level program in Haskell: type family NAryFn (n::Nat) (dom::*) (cod::*) :: * type instance NAryFn Ze dom cod = cod type instance NAryFn (Su n) dom cod = dom -> NA...
Rib asked 8/3, 2013 at 1:30

1

I'm trying to get a good grasp on Kinds, Types & Terms(or Values, not sure which is correct) and the GHC extensions for manipulating them. I understand that we can use TypeFamilies to write fun...
Directrix asked 19/2, 2013 at 2:50

© 2022 - 2024 — McMap. All rights reserved.