The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/15/2015 07:02 PM, Vilhelm Sjöberg wrote:
> On 2015-01-15 18:33, Jonathan Leivent wrote:
> > That does look familiar.  However, how to get 'get' to infer the ts 
> > arg from the tuple?  As this doesn't work:
> >
> >   get _ 2 (1, (true, (42, tt))).
> One way is to use typeclasses to infer this. The below code is 
> inspired by the Data.Typeable class in Haskell; I'm not sure if there 
> already is some existing similar framework in Coq.
>
>    Class Typeable (T : Set) := {
>      getCode : list Set;
>      getCode_spec : T = tupleType getCode
>    }.
>
>    Instance TypableUnit : Typeable unit :=
>      Build_Typeable unit nil eq_refl.
>
>    Instance TypeablePair (a b : Set) (c : Typeable b) : Typeable (a*b).
>       apply (Build_Typeable (a*b) (a::getCode)).
>       simpl. rewrite <- getCode_spec.
>       reflexivity.
>    Defined.
>
>    Definition cast {a b : Set} (p: a=b) (x: a) : b :=
>       match p in _=b return b with eq_refl => x end.
>
>    Definition get' {a:Set} {c: Typeable a} (i:nat) (v : a)  :=
>       get getCode i (cast getCode_spec v).
>
>    Eval compute in
>       get' 2 (1,(true,(42,tt))).  (* = 42 *)
>
> Vilhelm

This reminds me that I really need to learn me some typeclasses :-[

Can this be simplified by using a typeclass to overload get on pairs vs. 
every other type - and by doing so, ditch the tupleType completely?

-- Jonathan