[Haskell-cafe] writing a function to make a correspondance between type-level integers and value-level integers
TP
paratribulations at free.fr
Sun Jun 9 23:20:13 CEST 2013
> I'm hoping that gets you moving again and seeing this helps you piece it
> all together.
Thanks a lot Richard,
It helped me a lot to move forward. No doubt your answer will be very useful
for people looking for information on internet.
> - I changed the syntax of creating proxies. Instead of passing an
> argument, as you were trying, you set the type of a proxy using an
> explicit type annotation.
Indeed I did not realize that I could use `P::Proxy n`, and so that n does
not need to be argument of the data constructor `P`.
> - I added the extension ScopedTypeVariables, which allows method
> definitions to access type variables from an instance header.
In fact the extension ScopedTypeVariables is not needed to make your version
work. However, if I extend a bit your version like that:
-------------
data Tensor :: Nat -> * where
Tensor :: { order :: SNat order, name :: String } -> Tensor order
instance MkSNat o => Show (Tensor o) where
show Tensor { order = o, name = str } = str ++ " of order "
++ (show (mkSNat (P :: Proxy o))) --- (*1*)
--------------
and in the "main" part:
--------------
let vector = Tensor { order = mkSNat (P::Proxy order), name = "u" } ::
Tensor (Succ Zero)
print vector
---------------
then the line (*1*) makes mandatory to use the extension
ScopedTypeVariables. But I don't see the difference with your line:
---------------
instance MkSNat n => MkSNat ('Succ n) where
mkSNat _ = SSucc (mkSNat (P :: Proxy n))
---------------
So I don't understand why ScopedTypeVariables is needed in one case and not
in the other.
> - I added an extra constraint to the Succ instance for MkSNat, requiring
> that n is in the MkSNat class, as well.
I understand why we are compelled to use a constraint here:
---------------
instance MkSNat n => MkSNat ('Succ n) where
mkSNat _ = SSucc (mkSNat (P :: Proxy n))
---------------
My understanding is that we are compelled to put a constraint `MkSNat n`
because we cannot be sure that n (which is a type of kind Nat because type
constructor Succ takes a type of kind Nat as argument to make a concrete
type) is an instance of MkSNat because we are precisely defining this
instance.
However, why am I compelled to put a constraint in
---------------
instance MkSNat o => Show (Tensor o) where
show Tensor { order = o, name = str } = str ++ " of order "
++ (show (mkSNat (P :: Proxy o))) --- (*1*)
---------------
?
Indeed, we know that Tensor takes a type of kind Nat to make a concrete
type, so o is a type of kind Nat. And we have made `'Succ n` and `Zero`
instances of MkSNat; are we compelled to put a constraint because Haskell
makes the hypothesis that o could be another type of kind Nat different from
`'Succ n` and `Zero`? If yes, is it related to the sentence I have already
read: "Typeclasses are open"?
Thanks,
TP
More information about the Haskell-Cafe
mailing list