ryanglscott / eliminators Goto Github PK
View Code? Open in Web Editor NEWDependently typed elimination functions using singletons
License: BSD 3-Clause "New" or "Revised" License
Dependently typed elimination functions using singletons
License: BSD 3-Clause "New" or "Revised" License
(I hope term-level is the right expression...).
I have a HList:
data HList (ts :: [Type]) where
HNil :: HList '[]
(:&:) :: t -> HList ts -> HList (t ': ts)
infixr 5 :&:
And I want to write the following method:
length :: HList ts -> Sing (Length ts)
by not explicitly storing the length, but recursing on the HList(just like length
for the normal list) and "reflecting it back to the type-level (withSomeSing
)". Can I prove that this is correct (using eliminators)?
I don't see a way to do this.
I am wondering whether Eliminators can help prove that this is valid:
I have a normal HList:
data HList (ts :: [Type]) where
HNil :: HList '[]
(:&:) :: t -> HList ts -> HList (t ': ts)
infixr 5 :&:
instance (Show (HList '[])) where
show _ = "[]"
instance (Show a, Show (HList ts)) => (Show (HList (a : ts))) where
show (a :&: rest) = show a ++ ":&:" ++ show rest
and a homogenous case
newtype HoHeList (n :: Nat) a = HoHeList
{ unHoHeList :: HList (Replicate n a)
}
now, i want to create a show-instance:
instance Show a => Show (HoHeList (n :: Nat) a) where
show = (show . unHoHeList)
and prove it via (i am using your cong):
type TypeClassInduction a (n :: Nat) (f :: [Type] -> Type) (t :: Type -> Constraint)
= t (f (Replicate n a))
$(genDefunSymbols [''TypeClassInduction])
typeClassInduction :: forall (n :: Nat) (a :: Type) (f :: [Type] -> Type) (t :: Type -> Constraint).
(SingI n, t (f '[a]), forall xs x. (t (f xs), t x) => t (f (x ': xs)))
=> TypeClassInduction a n f t
typeClassInduction = elimNat @(TypeClassInduction a n f t) @n (sing @Nat @n) base step
where
base :: TypeClassInduction a 0 f t
base = Refl
step :: forall (k :: Nat).
Sing k
-> TypeClassInduction a k f t
-> TypeClassInduction a (k :+ 1) f t
step _ = case replicateSucc @k @a of
Refl -> cong @_ @_ @((:$$) (what should i pass here...i don't really understand :$$))
it seems like I could just use elimNat
again, but I am not sure. I get these errors that I am not sure how to solve:
$(genDefunSymbols [''TypeClassInduction])
results in
Expected kind ‘* -> Constraint’, but ‘t0’ has kind ‘* -> *’
removing it results genDefunSymbols
in
Expected a type, but
‘TypeClassInduction a n f t’ has kind
‘Constraint’
This is understandable since I am not returning a type, but instead a constraint. Is there a way to solve this?
(also, forall xs x. (t (f xs), t x) => t (f (x ': xs))
is not valid haskell...but it seemed natural to write)
Edit:
replicateSucc is defined as
axiom :: a :~: b
axiom = unsafeCoerce Refl
replicateSucc :: forall k a. Replicate (k :+ 1) a :~: (a : Replicate k a)
replicateSucc = axiom
eliminators
already defines elimNat
, which pretends Nat
is an inductive data type through clever use of unsafeCoerce
. Now that GHC 9.2+ defines a ConsSymbol
type family, we can define an analogous eliminator function for Symbol
.
Currently, I generate eliminators with predicates of two different kinds, <Datatype> -> Type
and <Datatype> ~> Type
, and I also have a story for eliminators that are polymorphic over the arrow kind used. However, I'm questioning whether all of this is worth it, since:
(~>)
variants anyway<Datatype> -> Type
can be turned into ones of kind <Datatype> ~> Type
without too much trouble (using the genDefunSymbols
function from singletons
)Perhaps we should only generate eliminators of kind <Datatype> ~> Type
.
The grand vision.
Coq generates different induction schemes depending on whether a data type inhabits Prop
or not:
Inductive evenA : nat -> Type :=
evenA0 : evenA 0
| evenASS : forall n, evenA n -> evenA (S (S n)).
Inductive evenB : nat -> Prop :=
evenB0 : evenB 0
| evenBSS : forall n, evenB n -> evenB (S (S n)).
Check evenA_ind.
(*
evenA_ind
: forall P : forall n : nat, evenA n -> Prop,
P 0 evenA0 ->
(forall (n : nat) (e : evenA n), P n e -> P (S (S n)) (evenASS n e)) ->
forall (n : nat) (e : evenA n), P n e
*)
Check evenB_ind.
(*
evenB_ind
: forall P : nat -> Prop,
P 0 ->
(forall n : nat, evenB n -> P n -> P (S (S n))) ->
forall n : nat, evenB n -> P n
*)
eliminators
should permit the generation of induction schemes à la evenB_ind
. (What should we call these?)
I am trying to proof the following:
type WhyDomainMatches a b (n :: Nat)
= ToDomain (Replicate n (a -> b)) :~: Replicate n a
where
type family ToDomain (xs :: [Type]) :: [Type] where
ToDomain '[] = '[];
ToDomain ((a -> b) ': r) = a ': ToDomain r
(Replicate is the usual Replicate form the singletons prelude)
through
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 _ = cong @_ @_ @((:$$) a)
I think that in theory this should work, cong
is copied from your tests, but GHC is not convinced yet.
Could not deduce: ToDomain
(Data.Singletons.Prelude.List.Case_6989586621679725646
(k GHC.TypeNats.+ 1)
(a -> b)
(GHC.TypeNats.EqNat (k GHC.TypeNats.+ 1) 0))
~
(a : ToDomain
(Data.Singletons.Prelude.List.Case_6989586621679725646
k (a -> b) (GHC.TypeNats.EqNat k 0)))
I've added (z :: Nat). (SingI n, (ToDomain (Replicate (z :+ 1) (a -> b)) ~ (a : ToDomain (Replicate (z) (a -> b)))))
to the constraints of domainMatches, but it didn't help, so I've also added it to step, but now I've got an error I can't really interpret:
Could not deduce: ToDomain
(Data.Singletons.Prelude.List.Case_6989586621679725646
(k GHC.TypeNats.+ 1)
(a -> b)
(GHC.TypeNats.EqNat (k GHC.TypeNats.+ 1) 0))
~
(a : ToDomain
(Data.Singletons.Prelude.List.Case_6989586621679725646
n (a -> b) (GHC.TypeNats.EqNat n 0)))
arising from a use of ‘step’
(why should k +1 equal n? There must be something wrong with my code!).
I've also got a second question, more fundamental. Assuming I get this to compile, how can I actually use this?
Also, cong & friends seem really useful and fundamental after a bit of searching, why are they not exported? They make the codebase pretty scary (I don't really understand what's going on), I think the actual Induction is surprisingly straightforward if you are familiar with the concept.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.