Comments (17)
Urk. I believe this is a GHC bug—in particular, Trac #11715—rearing its ugly head. In GHC Core, the Constraint
and Type
kinds are actually the same, which unfortunately means that there are certain places where GHC will confuse the two, such as Template Haskell reification. As a consequence, genDefunSymbols
will produce ill-kinded types, since the information it reified was itself ill-kinded.
I'm afraid the only workaround for the time being is to just create the defunctionalization symbols by hand:
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
import Data.Kind
import Data.Singletons
import Data.Singletons.Prelude.List
import GHC.TypeNats
type TypeClassInduction a (n :: Nat) (f :: [Type] -> Type) (t :: Type -> Constraint)
= t (f (Replicate n a))
data TypeClassInductionSym0 :: k ~> Nat ~> ([Type] -> Type) ~> (Type -> Constraint) ~> Constraint
data TypeClassInductionSym1 :: k -> Nat ~> ([Type] -> Type) ~> (Type -> Constraint) ~> Constraint
data TypeClassInductionSym2 :: k -> Nat -> ([Type] -> Type) ~> (Type -> Constraint) ~> Constraint
data TypeClassInductionSym3 :: k -> Nat -> ([Type] -> Type) -> (Type -> Constraint) ~> Constraint
type instance Apply TypeClassInductionSym0 a = TypeClassInductionSym1 a
type instance Apply (TypeClassInductionSym1 a) n = TypeClassInductionSym2 a n
type instance Apply (TypeClassInductionSym2 a n) f = TypeClassInductionSym3 a n f
type instance Apply (TypeClassInductionSym3 a n f) t = TypeClassInduction a n f t
from eliminators.
While I'm glad you found a solution, it now occurs to me that this is all completely overkill for the problem you're trying to solve. The root of the issue is that you have these two Show
instances for HList
:
instance (Show (HList '[])) where
show _ = "[]"
instance (Show a, Show (HList ts)) => (Show (HList (a : ts))) where
show (a :&: rest) = show a ++ ":&:" ++ show rest
These will only ever apply if you know statically that an HList
is empty or headed by (:)
. But that's not the case in your Show
instance for HoHeList
, which is why you were struggling to define it.
If I may, I'd like to propose a much simpler solution that doesn't use eliminators
at all:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where
import Data.Kind
import Data.Singletons.Prelude.List
import GHC.TypeNats
data HList (ts :: [Type]) where
HNil :: HList '[]
(:&:) :: t -> HList ts -> HList (t ': ts)
infixr 5 :&:
type family AllC (f :: Type -> Constraint) (xs :: [Type]) :: Constraint where
AllC _ '[] = ()
AllC f (x:xs) = (f x, AllC f xs)
deriving instance AllC Show xs => Show (HList xs)
newtype HoHeList (n :: Nat) a = HoHeList
{ unHoHeList :: HList (Replicate n a)
}
deriving instance AllC Show (Replicate n a) => Show (HoHeList n a)
The key here is in the use of AllC
. With this, you can define a single Show
instance for all HList
s, which makes defining a Show
instance for HoHeList
trivial. (You'll have to enable UndecidableInstances
for this trick to work, but whatever.)
Now maybe some day we can define AllC
by means of a type-level eliminator, but for the time being, you'll have to do the dirty work of defining it by direct recursion.
from eliminators.
Also, I have just played a bit around with your eliminators package a few months ago, but writing this was easy. I this would not be some constraint, but instead a normal type, I think I would have figured it out myself! 🙂
from eliminators.
okay, thank you!
But I am still not sure how I can do a induction over some constraint.
I can't return TypeClassInduction a n f t
....or can I (i am not really sure what's possible and what's not 😉)?
from eliminators.
I'm not sure either!
All of the code in this library is built around predicates p
such that p :: <datatype> ~> Type
. You're trying to use an exotic predicate of kind <datatype> ~> Constraint
, which certainly won't kind-check with the eliminators in this library. Moreover, I don't how one would even write a hypothetical eliminator that would support such a predicate. It's certainly not something I've ever seen in any dependently typed languages—are there examples out there of folks doing this sort of thing?
from eliminators.
I don't know either 😀 This was more out of need (all this hassle leads me trying to write a good old Show
-Instance).
I, unfortunately, have not much experience with "other" dependently typed languages, I have just played around with idris a bit and that's all.
from eliminators.
In any case, you're barking up the wrong tree with typeClassInduction
—it's not going to be well kinded either, as its return type is of kind Constraint
, not Type
, so it's not even a well formed function.
I suspect what you really want is something akin to a type-level eliminator. Something like:
type family ElimNatC (p :: Nat ~> Constraint) (s :: Nat) (pZ :: p @@ Z) (pS :: forall (n :: Nat). p @@ n -> p @@ (S n)) :: p @@ s where ...
Sadly, this is not possible in today's GHC, as its support for higher-ranked kinds in type families is extremely limited (see Trac #11719).
from eliminators.
yeah, I knew that this is not a well-defined function, I hoped there is something like :~:
for general constraints.
Hmm, so what can I do now? Any Idea? I don't think unsafeCoerce
will work...
from eliminators.
Hmm, so what can i do now?
Not much, I'm afraid. You're sailing through relatively uncharted waters on the fringes of GHC's type system, and you shouldn't be surprised if you hit impasses like this. There may be some other way to define your Show
instance, but one thing is clear: eliminators
aren't the solution (at present).
from eliminators.
Thank you for your patience 🙂
It's not only uncharted, I am also (not yet?) that knowledgable what my GHC is capable of and what's impossible.
from eliminators.
I don't want to bother you, but...could a different formulation of eliminators maybe work when i try something like like this?
(bogus, but my "inspiration")
type CanShow a n = HList (Replicate n a) -> String
$(genDefunSymbols [''CanShow])
canShowInduction :: forall (n :: Nat) (a :: Type) y (as :: [Type]).
(SingI n, Show a)
=> CanShow a n
canShowInduction = elimNat @(CanShowSym1 a) @n (sing @Nat @n) base step
where
base :: CanShow a 0
base = show
step :: forall (k :: Nat).
Sing k
-> CanShow a k
-> CanShow a (k :+ 1)
step _ _ = case replicateSucc @k @a of
Refl -> show
with a different formulation of step, so maybe something like this:
type ShowConstraint a n = Show (HList(Replicate n a))
type CanShow a n = HList (Replicate n a) -> String
$(genDefunSymbols [''CanShow])
canShowInduction :: forall (n :: Nat) (a :: Type) y.
(SingI n, Show a)
=> CanShow a n
canShowInduction = elimNat @(CanShowSym1 a) @n (sing @Nat @n) base step
where
-- (how can i get the (ShowConstraint a 0) from here?)
base :: CanShow a 0
base = show
step :: forall (k :: Nat). (ShowConstraint a k)
--- (ShowConstraint a k = Show(HList(Replicate a k))
Sing k
-> CanShow a (k :+ 1)
step _ = case replicateSucc @k @a of
-- (so we have (Replicate a (k + 1) ~ (a : Replicate a (k)))
Refl -> show
I don't know whether this would actually help or just move the problem into eliminators.
Also, I don't know whether GHC could figure it out, but I would guess so since show then exactly has the information it needs.
Another minor Problem here is that I can't replace it with an unsafeCoerce
using some rule, actually running them was not my intention 😀.
EDIT: I think not being able to just unsafeCoerce
this makes this impossible.
from eliminators.
I can't believe it...I've just solved it 😀 Eliminators is awesome!!
data Dict ctxt where
Dict :: ctxt => Dict ctxt
type TypeClassInduction a (f :: [Type] -> Type) (t :: Type -> Constraint) (n :: Nat)
= Dict (t (f (Replicate n a)))
-- due to https://ghc.haskell.org/trac/ghc/ticket/11715 we can't generate it
data TypeClassInductionSym0 :: k ~> ([Type] -> Type) ~> (Type -> Constraint) ~> Nat ~> Type
data TypeClassInductionSym1 :: k -> ([Type] -> Type) ~> (Type -> Constraint) ~> Nat ~> Type
data TypeClassInductionSym2 :: k -> ([Type] -> Type) -> (Type -> Constraint) ~> Nat ~> Type
data TypeClassInductionSym3 :: k -> ([Type] -> Type) -> (Type -> Constraint) -> Nat ~> Type
type instance Apply TypeClassInductionSym0 a = TypeClassInductionSym1 a
type instance Apply (TypeClassInductionSym1 a) f = TypeClassInductionSym2 a f
type instance Apply (TypeClassInductionSym2 a f) t = TypeClassInductionSym3 a f t
type instance Apply (TypeClassInductionSym3 a f t) n = TypeClassInduction a f t n
typeClassInduction :: forall (n :: Nat) (a :: Type) (f :: [Type] -> Type) (t :: Type -> Constraint).
(SingI n, t (f '[]), (t a))
=> (forall xs x. Dict (t (f xs)) -> Dict (t x) -> Dict (t (f (x ': xs)))) -> TypeClassInduction a f t n
typeClassInduction cStep = elimNat @(TypeClassInductionSym3 a f t) @n (sing @Nat @n) base step
where
base :: TypeClassInduction a f t 0
base = Dict @(t (f (Replicate 0 a)))
step :: forall (k :: Nat).
Sing k
-> TypeClassInduction a f t k
-> TypeClassInduction a f t (k :+ 1)
step _ prev = case replicateSucc @k @a of
Refl -> (cStep prev (Dict @(t a)))
usage
newtype HoHeList (n :: Nat) a = HoHeList
{ unHoHeList :: HList (Replicate n a)
}
instance (SingI n, Show a) => Show (HoHeList (n :: Nat) a) where
show :: forall xs. xs ~ (Replicate n a) => HoHeList n a -> String
show homogenous = let unhom :: HList xs = unHoHeList homogenous in
case typeClassInduction @n @a @HList @Show constrStep of
Dict -> show unhom
where
constrStep :: forall (a :: Type) (ts :: [Type]).
Dict (Show (HList ts)) -> Dict (Show a) -> Dict (Show (HList (a : ts)))
constrStep Dict Dict = Dict
ghci
*V2.HList> vals = 1 :&: 2 :&: 3 :&: HNil
*V2.HList> proveHomogenous vals
1:&:2:&:3:&:[]
*V2.HList> :t proveHomogenous vals
proveHomogenous vals :: Num t1 => HoHeList 3 t1
*V2.HList> hohe = proveHomogenous vals
*V2.HList> show hohe
"1:&:2:&:3:&:[]"
I just needed a bit of...creativity 😀 unbelievable that this works
EDIT: Do you know what actually happens when I run typeClassInduction
? The types all make sense...but I don't know whether the code actually does something.
from eliminators.
Do you know what actually happens when I run
typeClassInduction
? The types all make sense...but I don't know whether the code actually does something.
It certainly does something: it computes a Dict
—linearly in the size of n
, I might add. In other dependently typed languages, this might take constant time, since you could have an eta rule that says that all terms of type Dict
reduce to the Dict
constructor, but GHC does not have this ability due to the possibility of nontermination.
from eliminators.
Well, at least I learned something!
Here's something interesting: At least in GHCi, printing a HoHeList 2000 Nat
-List using my eliminator-based formulation is not noticeably slower than printing a replicate 2000 1
-list. But the normal Show, without your formulation, is super slow (it nearly crashes for me on a 2000 vector and consumes A LOT of memory (gigabytes!). It seems that the memory does grow exponential or at least has a big coefficient in front of it).
If I am not building first the type-level list and then convert it to a HoHeList
, but instead use
replicateH2 :: SNat n -> a -> HoHeList n a
replicateH2 n a =
HoHeList (unsafeCoerce (iterate (unsafeCoerce . (a :&:)) HNil
!! fromInteger (fromSing n)))
and then show it, I don't notice any slowdown between the eliminator-based show definition and not using not a type-level list. I can print homMany = replicateH2 (sing @Nat @200000) 1
.
I have not tested your approach yet and I don't have time until tomorrow, but I think it would require building the actual type-level list.
EDIT: Since I have a Functor
instance on my HoHeList
(stupid name 😀 ), also printing (+1) <$> homMany
seems IO-Bound. I am using these "proofs" and no Rewrite-Rules that eliminate them (seems like I don't need them?). They don't seem to not need noticable more space with increasing the HoHeList
size (coDomainMatches
is similiar formulated). At least I don't notice any, which is fine for now.
domainMatches :: forall (n :: Nat) (a :: Type) (b :: Type). SingI n => ToDomain (Replicate n (a -> b)) :~: Replicate n a
domainMatches = elimNat @(WhyDomainMatchesSym2 a b) @n (sing @Nat @n) base step
where
base :: WhyDomainMatches a b 0
base = Refl
step :: forall (k :: Nat).
Sing k
-> WhyDomainMatches a b k
-> WhyDomainMatches a b (k :+ 1)
step _ = case replicateSucc @k @(a -> b) of
Refl -> case replicateSucc @k @a of
Refl -> cong @_ @_ @((:$$) a)
This seems like a great opportunity for trying to figure out what GHC is doing (for the first time).
EDIT 2: yeah, deriving instance AllC Show (Replicate n a) => Show (HoHeList n a)
evaluates the whole list. There may be even smarter ways to implement this, but for now I am satisfied with my solution.
from eliminators.
Am I abusing the github ticket-system in your view? Is this even interesting to you?
from eliminators.
I don't think this is abusing GitHub at all! This stuff is far from obvious (both from a GHC programmer's perspective, and from the perspective of someone accustomed to dependent types in other languages).
I can't say I'm surprised to learn that code using elimNat
is inefficient—you're likely seeing the combined effect of inefficient Natural
code plus a complete lack of fusion that you're likely accustomed to for most data types, like lists. This library was intended to be a proof of concept, after all, and not a blazing-fast reference implementation! :)
If you're convinced that your proofs are correct, you can always make a rewrite RULE
to zap it away at runtime:
{-# RULES "typeClassInductionTerminates" typeClassInduction x = unsafeCoerce Dict #-}
I can't guarantee that's the only bottleneck in your code, but it would at least remove an obvious culprit.
from eliminators.
I think you misunderstood me (or I wasn't very clear)!
At least I was surprised how fast elimNat
is. This is working:
> homMany = replicateH2 (sing @Nat @200000) 1
> homMany
(just prints a lot of 1s)
> (+1) <$> homMany
(just prints a lot of 2s)
> foldr (+) 0 homMany
20000
(all 3 are using elimNat
)
where
replicateH2 :: SNat n -> a -> HoHeList n a
replicateH2 n a =
HoHeList (unsafeCoerce (iterate (unsafeCoerce . (a :&:)) HNil
!! fromInteger (fromSing n)))
to avoid actually building the type-level list. Having a type-level list of more than 2000 Elements starts eating all my RAM (so actually evaluating Replicate 2000 Nat
). I think I stopped at GHC using 10GB Ram.
I don't notice any slowdown compared to the just calling replicate
without type level stuff when using large lists.
from eliminators.
Related Issues (7)
- Generate eliminators using Template Haskell
- Should we bother generating eliminators with predicates of kind (<Datatype> -> Type)? HOT 1
- Unable to proof per Induction over Nat with Lists HOT 14
- eliminate term-level code HOT 2
- Emulate Coq's induction schemes for data types that inhabit Prop
- Add eliminator for `Symbol`
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from eliminators.