Questions tagged [type-level-computation]
A computation that is performed at compile time as part of the compiler's type checking phase.
type-level-computation
340
questions
53
votes
0
answers
1k
views
Materialize the Value for a Type that has One Inhabitant
Thanks to @MilesSabin's answer I can write a type level Fibonacci sequence:
sealed trait Digit
case object Zero extends Digit
case object One extends Digit
sealed trait Dense { type N <: Dense }
...
- 1,741
49
votes
5
answers
4k
views
Testing an assertion that something must not compile
The problem
When I'm working with libraries that support type-level programming, I often find myself writing comments like the following (from an example presented by Paul Snively at Strange Loop ...
- 139k
48
votes
1
answer
2k
views
Why is the Aux technique required for type-level computations?
I'm pretty sure I'm missing something here, since I'm pretty new to Shapeless and I'm learning, but when is the Aux technique actually required? I see that it is used to expose a type statement by ...
- 1,284
42
votes
1
answer
1k
views
Using the "Prolog in Scala" to find available type class instances
Considering https://speakerdeck.com/folone/theres-a-prolog-in-your-scala, I would like to "abuse" the Scala type system to find all instances of e.g. CanBuildFrom that match a given criteria. Prolog ...
- 37.5k
39
votes
3
answers
12k
views
What are some examples of type-level programming? [closed]
I do not understand what "type-level programming" means, nor can I find a suitable explanation using Google.
Could someone please provide an example that demonstrates type-level programming? ...
- 583
33
votes
2
answers
5k
views
Difference between Haskell and Idris: Reflection of Runtime/Compiletime in the type universes
So in Idris it's perfectly valid to write the following.
item : (b : Bool) -> if b then Nat else List Nat
item True = 42
item False = [1,2,3] // cf. https://www.youtube.com/watch?v=AWeT_G04a0A
...
- 1,905
23
votes
1
answer
849
views
Matching on type level Nat in GHC 7.6
My question is probably easiest to explain in the form of an example:
type family Take (n :: Nat) (xs :: [k]) :: [k]
type instance Take 0 xs = '[]
type instance Take (n+1) (x ': xs) = x '...
- 720
22
votes
1
answer
2k
views
Haskell singletons: What do we gain with SNat
I'm trying to grook Haskell singletons.
In the paper Dependently Typed Programming with Singletons
and in his blog post singletons v0.9 Released!
Richard Eisenberg defines the data type Nat which ...
- 1,679
19
votes
2
answers
686
views
Creating a fold that allows the type to change after each repeated function call, in order to call a function n times without recursion
I am trying to use a dfold defined here
dfold
:: KnownNat k
=> Proxy (p :: TyFun Nat * -> *)
-> (forall l. SNat l -> a -> (p @@ l) -> p @@ (l + 1))
-> (...
- 435
18
votes
1
answer
2k
views
Haskell Type Level Equality
Haskell has a resticted syntax to define type families:
(1) type family Length (xs :: [*]) where
(2) Length '[] = 0
(3) Length (x ': xs) = 1 + Length xs
On the lines (2) and (3) on the ...
- 1,679
18
votes
3
answers
926
views
Are there "type-level combinators"? Will they exist in some future?
Much of what makes haskell really nice to use in my opinion are combinators such as (.), flip, $ <*> and etc. It feels almost like I can create new syntax when I need to.
Some time ago I was ...
- 13.8k
16
votes
3
answers
664
views
Applying a fixed-length-vector-function to the inital part of a longer fixed-length-vector
I have the following definition of fixed-length-vectors using ghcs extensions GADTs, TypeOperators and DataKinds:
data Vec n a where
T :: Vec VZero a
(:.) :: a -> Vec n a -> Vec (...
- 4,890
16
votes
1
answer
3k
views
How does haskell resolve overlapping instances?
Please excuse me if I use the wrong terminology, I am much a beginner in haskell type manipulation... I am trying to use overlapping instances with functional dependencies to do some type-level ...
- 2,439
14
votes
4
answers
895
views
Generate function of given arity in Haskell using type numbers
Assume I have encoded the natural numbers in Haskell types, and that I have a way of adding and subtracting from them:
data Zero
data Succ n
-- ...
I have seen various bits of code which create the ...
- 18.3k
14
votes
1
answer
382
views
haskell - generate an instance for all classes except one specific type
Is it possible to do something like
class T a
class U a
instance U ()
instance ( NOT U a ) => T a
Context: I am trying to write a function that takes HLists and removes elements of a certain ...
- 2,439
13
votes
1
answer
1k
views
Explain the `LowPriorityImplicits` pattern used in Scala type-level programming
When looking at the source of some Scala libraries, e.g. shapeless, I often find traits named LowPriorityImplicits.
Can you please explain this pattern? What is the problem that is solved, and how ...
- 28.5k
13
votes
1
answer
170
views
Is there a way to get a compile-time error if there's no matching closed type family instance?
I have a closed type family which has no catch-all case:
{-# LANGUAGE TypeFamilies #-}
type family Foo a where
Foo Bool = Int
Foo Int = Bool
Is there a way to force the type checker to ...
- 27.3k
11
votes
2
answers
898
views
What is the purpose of the emptyCoproduct and coproduct methods of the TypeClass trait in Shapeless
It is not fully clear to me what is the purpose of the emptyCoProduct and coproduct methods of the TypeClass trait in Shapeless.
When would one use the TypeClass trait instead of the ProductTypeClass?...
- 3,013
11
votes
1
answer
971
views
Scala type level programming - representing a hierarchy
I'm learning about type level programming in Scala and I'm curious if it's possible to represent a tree or hierarchy using type level programming.
The simple case would be a multi-level tree
A_
|
...
- 7,764
11
votes
2
answers
1k
views
Exporting type-operators from modules
How do you export type-operators? Considering they can clash with normal operators, there must be a special syntax if it's possible.
- 1,979
11
votes
1
answer
652
views
Scala Shapeless Code for Project Euler #1
I am new to shapeless and have been trying to practice some type level programming. I took Problem #1 from Project Euler as my first challenge.
I started by writing regular scala code:
object ...
- 1,741
11
votes
2
answers
807
views
In GHC.TypeLits what is someNatVal good for (which we can't accomplish with natVal)?
I'm trying to understand GHC.TypeLits, and specifically someNatVal. I understand the way it's used in this blog post here, but as mentioned the same example could have been implemented using natVal, ...
- 16.5k
11
votes
1
answer
629
views
scala path dependent types and type level proofs
I am currently trying to define a model of a clocked dataflow language in scala.
A flow virtually represents an infinite sequence of values of some type T, paced by some clock C (a clock indicates ...
- 566
10
votes
1
answer
317
views
Change fixity of function type (->)?
Doing some type-level computation I've come to a point where I want to change the fixity of -> because it can't be mixed with left associative type operators of fixity 0. I know it doesn't work ...
- 1,979
10
votes
1
answer
308
views
How can I extract this polymorphic recursion function?
I'm doing so fairly fun stuff with GHC 7.8, but have ran in to a bit of a problem. I have the following:
mkResultF :: Eq k => Query kvs ('KV k v) -> k -> ResultF (Reverse kvs) (Maybe v)
...
- 6,030
10
votes
1
answer
282
views
Scala type constraint to check argument values
I'm trying to implement Conway's surreal numbers in Scala. A surreal number is defined recursively – as a pair of sets of surreal numbers, called left and right, such that no element in the right set ...
- 103
10
votes
1
answer
281
views
How to prove double negation for type level booleans?
I have the following module:
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, RoleAnnotations #-}
module Main where
import Data.Coerce (coerce)
-- logical negation for type level booleans
type ...
- 3,403
9
votes
3
answers
2k
views
Shapeless HList type checking
I am using Shapeless and have the following method to compute the difference between two HLists:
def diff[H <: HList](lst1: H, lst2:H):List[String] = (lst1, lst2) match {
case (HNil, HNil) ...
- 4,471
9
votes
2
answers
658
views
Why does my functional dependency conflict disappear when I expand the definition?
I was trying to implement Integers at the type level in Haskell. To start I implemented natural numbers with
data Zero
data Succ a
I then extended this to the integers with
data NegSucc a
I ...
- 4,051
9
votes
1
answer
193
views
Creating a completely dependent concatenation
A nice true fact about concatenation is that if I know any two variables in the equation:
a ++ b = c
Then I know the third.
I would like to capture this idea in my own concat so I use a functional ...
- 4,051
9
votes
1
answer
239
views
Vinyl: compose record type aliases
In Vinyl, I can define a type alias for a record to make it easier to export to other modules:
import Data.Vinyl
name = Field :: "name" ::: String
age = Field :: "age" ::: Int
type Person = ["name" :...
- 5,059
9
votes
1
answer
167
views
Numeric type signature
Is it possible to create a type with a numeric argument?
i.e. if I want to create a type of integers with a fixed bit-width:
newtype FixedWidth w = FixedWidth Integer
addFixedWidth :: FixedWidth w -...
- 12.6k
9
votes
3
answers
538
views
Experience reports using indexed monads in production?
In a previous question I discovered the existence of Conor McBride's Kleisli arrows of Outrageous Fortune while looking for ways of encoding Idris examples in Haskell. My efforts to understand McBride'...
- 4,598
9
votes
2
answers
1k
views
Haskell type family instance with type constraints
I am trying to represent expressions with type families, but I cannot seem to figure out how to write the constraints that I want, and I'm starting to feel like it's just not possible. Here is my ...
- 101
9
votes
1
answer
805
views
When to use existential type vs. dependent pair in Haskell?
When would one want to use a specialized existential type vs. a dependent pair (also called a dependent sum or sigma type)?
Here is an example.
The following is a length-indexed list and dependently-...
- 3,598
9
votes
1
answer
835
views
haskell - How can I go from values to types?
Imagine I have the following data types and type classes (with proper language extensions):
data Zero=Zero
data Succ n = Succ n
class Countable t where
count :: t -> Int
instance Countable ...
- 2,439
9
votes
3
answers
334
views
how to create custom type error on constraint violation
I have a class instance that has some relatively unintuitive constraints. This results in unreadable error messages if this constraint is violated. What I would like to do is provide a custom type ...
user2882307
9
votes
1
answer
163
views
Can I get GHC to infer a constraint past a GADT pattern match?
I would like to get GHC to infer a constraint past a GADT pattern match. For instance, suppose I have two expressions, each with an inferred constraint:
f :: _ => a
g :: _ => a
(In my use case, ...
- 719
8
votes
3
answers
413
views
Bidirectional Functional Dependencies
I have a type class that looks a bit like the following:
class Foo a b | a -> b where
f :: a -> Bool
g :: b -> Bool
h :: a -> b -> Bool
Or at least these are the bits that are ...
- 4,051
8
votes
2
answers
854
views
What is '[] and ': in Haskell?
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 :: [*]) ...
- 1,991
8
votes
2
answers
409
views
How to trigger a type family pattern match error in Haskell?
Is Haskell able to indicate a type family match error? For example, using a closed type family:
type family Testf a where
Testf Char = IO ()
Testf String = IO ()
The type of Testf Int is just ...
- 1,955
8
votes
1
answer
372
views
What is this Haskell Syntax (type level operators?)
What does '[] or ': signify in Haskell code? Some examples -
Example 1:
data OrderPacket replies where
NoOrders :: OrderPacket '[]
Example 2:
data Elem :: [a] -> a -> * where
EZ :: Elem ...
- 7,951
8
votes
1
answer
372
views
Is there any connection between `a :~: b` and `(a :== b) :~: True`?
Is there any connection implemented between propositional and promoted equality?
Let's say I have
prf :: x :~: y
in scope for some Symbols; by pattern matching on it being Refl, I can transform ...
- 27.3k
8
votes
2
answers
377
views
Behavior of type level naturals in GHC 7.8
If you want vectors indexed by their length you can do something like this:
{-# LANGUAGE
DataKinds, GADTs, TypeOperators, TypeFamilies, StandaloneDeriving
#-}
data N = P N | Z
type family Add ...
- 14.6k
8
votes
1
answer
1k
views
In Scala, is it possible to "curry" type parameters of a def?
Let's suppose I have a def that takes multiple type parameters:
def foo[A, B, C](b: B, c: C)(implicit ev: Writer[A])
However, the intended usage is that type parameters B and C should be inferred (...
- 2,962
8
votes
1
answer
426
views
Type safe lookup on heterogeneous lists in Haskell
I want to develop a type safe lookup function for the following data type:
data Attr (xs :: [(Symbol,*)]) where
Nil :: Attr '[]
(:*) :: KnownSymbol s => (Proxy s, t) -> Attr xs -> ...
- 3,198
8
votes
2
answers
339
views
Map Shapeless hlist type F[T1] :: ... :: F[Tn] :: HNil to the type T1 :: ... :: Tn :: HNil (type level sequencing)
I'm building a generic function that takes in a HList of the form F[T1] :: ... :: F[Tn] :: HNil, converts that into a F[T1 :: ... :: Tn :: HNil] and then needs to pass that into a block that was ...
- 37.5k
8
votes
1
answer
346
views
Why doesn't this code infringe the "saturation requirement of type families"?
I have this minimal working example (culled from the singletons library) of mapping a type family over a type-level list:
{-# language PolyKinds #-}
{-# language DataKinds #-}
{-# language ...
- 27.1k
7
votes
3
answers
2k
views
how to write an `Invert` type in typescript to invert the order of tuples
type a = [1,2,3]
type Invert<T extends any[] & {'0': any}> = ???
type b = Invert<a> // should yield [3,2,1]
I am stucked to figure out the definition of Invert type of a tuple,
also ...
- 993
7
votes
1
answer
2k
views
mapping over HList inside a function
The following code seems obvious enough to compile and run
case class Pair(a: String, b: Int)
val pairGen = Generic[Pair]
object size extends Poly1 {
implicit def caseInt = at[Int](x => 1)
...
- 73