data-kinds Questions
1
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...
Handler asked 14/1, 2018 at 15:21
0
The following code tries to refine Clash's Unsigned type family at index 4 into Digit:
import Clash.Prelude
{-@ type Digit = {v : Unsigned 4 | v <= 9 } @-}
type Digit = Unsigned 4
{-@ foo :: D...
Nought asked 18/9, 2022 at 10:51
2
Solved
In Maguire's Thinking with Types, p. 29, there's an example of how to use a promoted data constructor as a phantom parameter. Here's a module that I wrote based on the example in the book.
{-# LANG...
Encompass asked 17/9, 2021 at 16:38
1
Solved
Why does addition, subtraction and division of Nats work, but not multiplication?
λ> :set -XDataKinds
λ> :set -XTypeOperators
λ> import GHC.TypeLits
λ> :k! 1 + 2
1 + 2 :: Nat
= 3
λ> ...
Intercontinental asked 17/9, 2021 at 19:55
3
Solved
I'm trying to use a GADT with DataKinds, as shown below
{-# LANGUAGE KindSignatures, DataKinds, GADTs #-}
module NewGadt where
data ExprType = Var | Nest
data Expr (a :: ExprType) where
ExprVar ...
Cower asked 10/9, 2021 at 21:42
2
I would like to define a data type in Haskell which is parametrized by an Int constant along the lines:
data Q (n :: Int) = Q n (Int,Int) -- non-working code
in order to allow me to define function...
Dever asked 15/3, 2021 at 15:52
1
Solved
I'm currently going through Sandy Maguire's Thinking with Types, and chapter 2 covers Terms, Types and Kinds. In it, there's an example of a simple interaction with the type-level primitives for pe...
Esotropia asked 12/5, 2020 at 6:48
1
Solved
Using DataKinds and TypeOperators, I can make type level-tuples of types, and type-level lists of types, but I cannot nest them:
> :k '['(Int, Int), '(Int, Int)]
error: parse error on input ‘'’...
Agglutinogen asked 18/2, 2020 at 19:21
3
Consider following definition of a HList:
infixr 5 :>
data HList (types :: [*]) where
HNil :: HList '[]
(:>) :: a -> HList l -> HList (a:l)
And a type family Map to map over typele...
Depressor asked 17/9, 2019 at 11:16
2
Solved
Say I have the following:
data Type
= StringType
| IntType
| FloatType
data Op
= Add Type
| Subtract Type
I'd like to constrain the possible types under Subtract, such that it only allows ...
Coquetry asked 7/4, 2019 at 5:59
4
Solved
I'm not sure if it is the right terminology, but is it possible to declare function types that take in an 'union' of datakinds?
For example, I know I can do the following:
{-# LANGUAGE DataKinds ...
Watchman asked 16/2, 2019 at 5:3
2
Solved
I've seen this '[] and ': syntax in a few places, most notably in heterogeneous lists packages like HList or HVect.
For example, the heterogeneous vector HVect is defined as
data HVect (ts :: [*]...
Jola asked 3/1, 2019 at 10:21
2
Solved
I learn type programming of Haskell from Basic Type Level Programming in Haskell but when it introduce DataKinds extension, there are something seems confusing from the example:
{-# LANGUAGE DataK...
Glutenous asked 17/12, 2018 at 9:52
1
Solved
I'm trying to implement a CurrencyQty type that acts like a number tagged at compile time:
data Currency = Usd | Eur | Gbp
data CurrencyQty (a :: Currency) = CurrencyQty Double deriving (Num)
A...
Madelinemadella asked 12/9, 2018 at 16:11
1
Solved
So, ghci is giving me an interesting error when I try and pin down the type of a polymorphic return value when using DataKinds. I have the following code:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE K...
Goldofpleasure asked 4/1, 2017 at 16:54
2
Solved
I'm relatively new to Haskell, and I'm trying to understand one of the definitions of HList.
data instance HList '[] = HNil
newtype instance HList (x ': xs) = HCons1 (x, HList xs)
pattern HCons x ...
Hardback asked 14/12, 2016 at 5:4
1
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 int...
Overburden asked 21/11, 2016 at 22:1
1
Solved
I'm trying to create a type that guarantees that a string is less than N characters long.
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{...
Rifleman asked 21/11, 2016 at 23:19
2
Solved
I'm writing a lib for message queues. Queues can be either Direct or Topic. Direct queues have a static binding key, while Topic queues can have dynamic ones.
I want to write a function publish t...
Photochromy asked 12/10, 2016 at 21:0
2
Solved
I am trying to gork the tutorial for the servant library, a type-level web DSL. The library makes extensive use of the DataKind language extension.
Early in that that tutorial we find the followin...
Medial asked 4/5, 2016 at 1:11
1
Solved
I'm getting an error when trying to define a pattern synonym based
on a GADT that has a type-level list.
I managed to boil it down to this example:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatu...
Gulgee asked 30/3, 2016 at 22:24
2
Solved
I'm studying the type family features of Haskell, and type level computation.
It appears it's quite easy to get parametric polymorphism at the type-level using PolyKinds:
{-# LANGUAGE DataKinds, T...
Arboreal asked 18/3, 2016 at 8:37
1
Solved
Is there some reason why this code is not compiled:
type family Foo a b :: Bool where
Foo a b = a == b
foo :: Foo a b ~ True => Proxy a -> Proxy b
foo _ = Proxy
bar :: Proxy a -> Proxy...
Luxuriant asked 3/2, 2016 at 8:15
2
Solved
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) '...
Johnnyjumpup asked 21/12, 2015 at 16:38
1
Solved
I'd like to make a typed AST for a dynamic language. At present, I'm stuck on handling collections. Here's a representative code sample:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGU...
Nicknickel asked 14/12, 2015 at 4:21
1 Next >
© 2022 - 2024 — McMap. All rights reserved.