Questions tagged [higher-rank-types]
Higher rank types are types containing type variables that are locally quantified. Type inference for such types is not decidable.
99
questions
0
votes
1
answer
31
views
Using HRTBs to automate getter method unit tests
I have a "view" data structure in Rust that contains a reference to another data structure, and I want to automate testing of the getter methods that I implemented on the view data structure....
0
votes
0
answers
86
views
Bound for reference of associated type
I need an associated type that is bound to be "any kind of collection" (i.e. anything that has a .iter() method). Now, .iter() in rust collections isn't part of a trait usually, but ...
3
votes
1
answer
143
views
Is it possible to infer a type that is a reflection-like closure?
With the following "toy model" of Clash:
{-# LANGUAGE RankNTypes, KindSignatures, DataKinds, FlexibleContexts #-}
-- Simplified model of platform definitions
data Domain = DomSys | Dom25
...
3
votes
1
answer
106
views
Rust: additional trait bounds in conjunction with higher-ranked lifetime bounds
I want trait implementations in Rust to be able to return arbitrary iterators (of specific item type) that may reference the original object with a lifetime 'a without having to explicitly mention 'a ...
5
votes
1
answer
77
views
Flipping with rank-N types
I have the following Rank 2 function:
polyOn :: (f a -> f b -> c) -> (forall k . k -> f k) -> a -> b -> c
polyOn bifunc func x y =
bifunc (func x) (func y)
I'd like to flip it
...
4
votes
2
answers
75
views
How to construct values of a higher-rank Coyoneda type in CPS?
{-# LANGUAGE RankNTypes #-}
newtype Coyoneda f a = Coyoneda {
uncoyo :: forall b r. ((b -> a) -> f b -> r) -> r
}
coyoneda f tx = Coyoneda (\k -> k f tx)
I think Coyoneda should ...
4
votes
1
answer
94
views
Coyoneda hasn't a higher-rank type but what type has it actually?
Yoneda has a valid type as long as the higher-rank extension is set:
newtype Yoneda f a = Yoneda (forall b. (a -> b) -> f b) which yields the type (forall b. (a -> b) -> f b) -> Yoneda ...
1
vote
1
answer
28
views
How to use Higher Rank Trait Bounds with anonymous closure in return type
Is it possible to return FnMut closure that takes reference and return reference with same lifetime as it takes?
fn fun(buf: &mut [f32], mut idx: usize) -> impl FnMut(&[i16]) -> &[...
2
votes
1
answer
98
views
How to reproduce GHC's type error for a rigid type variable escaping its scope?
Here is the canonical example for a rigid type variable escaping its scope:
{-# LANGUAGE RankNTypes #-}
runST :: forall a. (forall s. ST s a) -> a
runST _ = undefined
newRef :: forall s a. a -> ...
5
votes
1
answer
90
views
How does instantiation of higher-rank types and subsumption interact during unification?
A function type is higher-rank if a quantifier appears in contravariant position: f :: (forall a. [a] -> b) -> Bool
Regarding the unification of such a type the type variable a is more rigid ...
1
vote
1
answer
78
views
How is the scope of a nested universal quantifier determined (higher-rank types)?
Originally I assumed the scope of a nested universal quantifier on the LHS of a function type can be determined purely syntactical, i.e. everything inside the parenthesis of (forall a. a -> b) ->...
5
votes
2
answers
160
views
How to infer the type of the Scott encoded List constructor?
Scott encoded lists can be defined as followed:
newtype List a =
List {
uncons :: forall r. r -> (a -> List a -> r) -> r
}
As opposed to the ADT version List is both type ...
0
votes
2
answers
63
views
Is there any way to map over a collection of values of a type parameterized with a higher type?
I read existing questions about how type definitions with parameterized bounds are illegal inside blocks (or something to that effect), but it doesn't help me in my problem:
type Cons[X]
class Higher[...
4
votes
1
answer
528
views
Higher ranked trait bounds and function parameters
I'm trying to understand the implementation of Bevy's IntoForEachSystem trait and the way it interacts with the underlying Hecs Query and Fetch traits. Hecs has query types (the thing you request in a ...
1
vote
2
answers
74
views
Haskell Rank1Types and parentheses -- strange behaviour
Switching on RankNTypes (without which these signatures won't get accepted, because they're not Haskell 98, says the User Guide), and -fprint-explicit-foralls so I can see the quantification, consider:...
12
votes
4
answers
1k
views
How do I return an associated type from a higher-ranked trait bound trait?
I have a trait that has a function for deserializing an associated type. However that associated type needs to have a lifetime that the caller decides, so I have a separate trait that I use a higher-...
4
votes
0
answers
256
views
Polymorphic closures in Rust
I'm starting to learn Rust (apologies in advance) and I'm trying to implement a monadic parser combinator library. Parsers implement a Parser trait as follows:
// parse success is a value + the rest ...
10
votes
2
answers
231
views
Juggling existentials without unsafeCoerce
Lately I have been playing with this type, which I understand to be an encoding of the free distributive functor (for tangential background on that, see this answer):
data Ev g a where
Ev :: ((g ...
3
votes
2
answers
161
views
Why is this type annotation wrong?
I tried to follow the article by Gabriel Gonzalez and I ran into a type mismatch. Consider the following short module:
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE Rank2Types #-}
module Yoneda where
...
1
vote
1
answer
122
views
How to work around a HRTB bug?
This snippet does not compile because of a compiler bug:
struct Theory<'a, T: 'a> {
left: &'a T,
}
pub struct Contain<'a, T: 'a, U>
where
&'a T: IntoIterator,
for<'...
2
votes
2
answers
521
views
Illegal polymorphic or qualified type in Haskell
Why is Haskell complaining when trying to parse this type signature?
f :: (a,s) -> (forall r.(r -> (a,r)),s)
2
votes
2
answers
134
views
On nested CPS suspension types
Let's begin with the familiar type of CPS suspended computations, (a -> r) -> r, spelled as Cont r a in mtl-speak. We know that it is isomorphic to a as long as it is kept polymorphic in r. If ...
14
votes
1
answer
215
views
Vector creation safety
This question is actually a small lattice of very closely related questions; I don't think it makes much sense to break it up as yet.
One of the fundamental ways to create a Vector is using ...
6
votes
1
answer
146
views
Can type classes at the type level be simulated with higher-rank types?
I have a pluggable runtime type checker that supports parametric but no ad-hoc polymorphism, because there is no compiling step and type information are erased as soon as the type checker is ...
1
vote
1
answer
66
views
How to use a Reader type encoded with continuation passing style
I was under the impression that every value of type a can be described with a rank-2 polymorphic type newtype Id a = Id {runId :: forall r. (a -> r) -> r } in continuation passing style. So I ...
10
votes
2
answers
385
views
Why are explicit forall quantifiers necessary for rank-n types?
When I declare this newtype:
newtype ListScott a =
ListScott {
unconsScott :: (a -> ListScott a -> r) -> r -> r
}
which would define the hypothetical rank-2 type ListScott :: ((a -...
0
votes
1
answer
153
views
Why can't GHC deduce type equality on a class type family in a Rank 2 type?
As a very trimmed-down version of what I'm experiencing:
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
class ValueGen v where
type Output v
generate :: ...
3
votes
0
answers
161
views
Can I implement an heterogeneous list based on an existential with Church encoding and Rank-N types?
In my attempt to understand existential types I've read that Church encoding along with the Rank-N-types extension would be sufficient to encode them in Haskell without existential quantification. I ...
6
votes
1
answer
109
views
How to non-impredicatively return `Maybe` a lens?
A type like Maybe (Lens' a b) doesn't work because Lens' is under the hood a Rank-2 type, that can't be wrapped in a type constructor without the -XImpredicativeTypes extension (which is not really ...
0
votes
1
answer
267
views
Could not deduce (TypeClass a0) arising from a use of ‘variable’
I have a type:
type DifferentiableFunction n a = (Function n a, List n (Function n a), String)
Elsewhere I define:
data Something where
Operator :: Something -> (forall a . Floating a => ...
2
votes
1
answer
100
views
Pattern matching inferred type
Why doesn't the below type-check? The type of _ is inferred as Double.
{-# LANGUAGE ScopedTypeVariables, Rank2Types #-}
module Main (main) where
data D a = D a
main =
let
n = D (1 :: forall ...
1
vote
1
answer
164
views
Rank-1 Type requires Rank2Types extension
Haskell wiki page on Rank-N-Types tells that this type
forall a . a -> (forall b . b -> a)
has Rank 1. I believe in this fact and it seems quite understandable for me (keeping in mind what I ...
5
votes
1
answer
152
views
RankNTypes and Church numerals
I'm trying to study church numerals in Haskell by giving the numbers a type like this, with the idea that a natural number n is basically the expression that applies the function in the following type ...
16
votes
1
answer
201
views
The case of the disappearing constraint: Oddities of a higher-rank type
All the experiments described below were done with GHC 8.0.1.
This question is a follow-up to RankNTypes with type aliases confusion. The issue there boiled down to the types of functions like this ...
3
votes
1
answer
176
views
RankNTypes with type aliases confusion [duplicate]
I'm trying to understand how type constraints work with type aliases. First, let's assume I have next type alias:
type NumList a = Num a => [a]
And I have next function:
addFirst :: a -> ...
4
votes
1
answer
191
views
Is it possible to 'uncurry' a forall quantifier?
Suppose we have a type constructor f that takes two types, by means of a DataKinds-promoted pair.
forall (f :: (ka, kb) -> *)
I can then implement a function forward, which is like curry for the ...
9
votes
2
answers
648
views
Why are higher rank types so fragile in Haskell
I was messing around with the runST function. Which has type (forall s. ST s a) -> a and it seems like trying to use it in any way that isn't directly applying without any indirection breaks it in ...
1
vote
1
answer
120
views
How to assign a value from the IO monad to a RankNType qualified constructor
(UPDATED)
I have made an interface using a Free Monad to a generic data store. I want to place the specific interpreter (:: DataStore a -> IO a) chosen by the user at run time into a state monad ...
11
votes
2
answers
195
views
What is the name of this functor that uses RankNTypes?
During play around objective package, I noticed following type has interesting property.
> {-# LANGUAGE RankNTypes #-}
> data N f r = N { unN :: forall x. f x -> (x, r) }
It is a Functor.
&...
2
votes
1
answer
64
views
Unwrapping the STT monad in a transformer stack?
This question is apparently related to the problem discussed here and here. Unfortunately, my requirement is slightly different to those questions, and the answers given don't apply to me. I also ...
2
votes
2
answers
687
views
Purely Applicative Parser using Alternative
In a previous post, a user offered an implementation of a purely applicative parser for Haskell (code originally from here). Below is the partial implementation of that parser:
{-# LANGUAGE ...
2
votes
1
answer
76
views
What does the error message "Universe inconsistency" mean when working with higher-rank types?
Given the following Idris code:
import Data.Vect
import Data.Fin
%default total
fins : Vect n (Fin n)
fins {n = Z} = []
fins {n = S n} = FZ :: map FS fins
Permutation : Nat -> Type
Permutation ...
13
votes
1
answer
176
views
Why is `[1, "a"] :: [forall a. Show a => a]` not allowed?
In my (might incorrect) understanding, following two lists should be equivalent:
[1, "a"] :: [forall a. Show a => a]
data V = forall a. Show a => V a
[V 1, V "a"] :: [V]
However, the first ...
3
votes
1
answer
614
views
Rank-2 types in data constructors
I've been trying to encode GADTs in PureScript using rank-2 types, as described here for Haskell
My code looks like:
data Z
data S n
data List a n
= Nil (Z -> n)
| Cons forall m. a (List a ...
2
votes
1
answer
244
views
rankntypes: Illegal polymorphic or qualified type
I am trying to expand (or trying to find out whether it's possible to expand) a function with a type signature that already goes to the limits of my knowledge, because of the libraries I'm using which ...
12
votes
3
answers
533
views
How should the general type of a "lemma" function be understood?
Perhaps this is a stupid question. Here's a quote from the Hasochism paper:
One approach to resolving this issue is to encode lemmas, given by
parameterised equations, as Haskell functions. In ...
8
votes
1
answer
138
views
How does let interact with higher rank types in Haskell?
I ran in to a puzzling situation with a higher rank type. I figured out how to make it work, but I don't understand the difference between the working and non-working versions.
With these background ...
4
votes
1
answer
272
views
Type error with rank-n types and lenses
I have a simple polymorphic datatype Foo
{-# LANGUAGE TemplateHaskell #-}
import Control.Lens
data Foo c =
Foo {
_bar :: c,
_baz :: c,
_quux :: c
}
makeLenses ''...
13
votes
3
answers
2k
views
RankNTypes and PolyKinds
What is the difference between f1 and f2?
$ ghci -XRankNTypes -XPolyKinds
Prelude> let f1 = undefined :: (forall a m. m a -> Int) -> Int
Prelude> let f2 = undefined :: (forall (a ::...
-1
votes
1
answer
692
views
Ranking or Position on value of multidimensional array in PHP
I want to rank this following array according to points and duplicate points will be same ranked. Any idea how I will be complete this task.
Array
(
[6] => Array
(
[points] => 0
...