@d_christiansen @acid2 The type seems incorrect and unnecessarily restricted, too:
(~>) : (a -> Type) -> (a -> Type) -> a -> Type
-
-
Replying to @ertesx
@ertesx@d_christiansen@acid2 I thought (in agdris, apols) (~>) : (I -> Type) -> (I -> Type) -> Type (~>) {I} F G = (i : I) -> F i -> G i.2 replies 0 retweets 1 like -
Replying to @pigworker
@pigworker@d_christiansen@acid2 Wow, that looks weird. My Agda instinct does not like the pseudo-implicit i.1 reply 0 retweets 0 likes -
Replying to @ertesx
@ertesx@d_christiansen@acid2 In Agda, _~>_ : {I : Set} -> (I -> Set) -> (I -> Set) -> Set F ~> G = forall {i} -> F i -> G i2 replies 0 retweets 0 likes -
Replying to @pigworker
@pigworker@ertesx@d_christiansen@acid2 In idris: (~>) : {i : Type} -> (i -> Type) -> (i -> Type) -> Type f ~> g = {i : _} -> f i -> g i3 replies 0 retweets 0 likes -
Replying to @edwinbrady
@edwinbrady@pigworker@d_christiansen@acid2 Once feature of the RankNTypes version is that f ~> g takes another type argument. Same here?1 reply 0 retweets 0 likes -
Replying to @ertesx
@edwinbrady@pigworker To elaborate: Let (f : {A} → B → C) does (f x) take another argument or is it of type C?1 reply 0 retweets 0 likes -
Replying to @ertesx
@ertesx@pigworker f x is of type C. I just translated this code with no attempt to understand it…1 reply 0 retweets 0 likes -
Replying to @edwinbrady
@edwinbrady@pigworker Then it will probably not do what a Haskeller would expect with RankNTypes: f :: (∀ a. F a -> G a) → …1 reply 0 retweets 0 likes -
Replying to @ertesx
@ertesx@edwinbrady Insufficient bandwidth. No clue what's going on.2 replies 0 retweets 0 likes
@pigworker @ertesx Me neither. It only wants one explicit argument because that's what the type said. Are we talking about different things?
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.