[Haskell-beginners] Type depending on value
Dmitriy Matrosov
sgf.dma at gmail.com
Mon Apr 11 11:32:30 UTC 2016
> {-# LANGUAGE DataKinds, KindSignatures, GADTs, StandaloneDeriving #-}
Hi.
Here is natural numbers and its singleton definition, which i take from
"Part
I: Dependent Types in Haskell" article by Hiromi ISHII [1]:
> data Nat = Z | S Nat
> deriving (Show)
>
> data SNat :: Nat -> * where
> SZ :: SNat 'Z
> SN :: SNat n -> SNat ('S n)
> deriving instance Show (SNat n)
But i can't figure out how may i define function returning SNat value
depending on Nat value:
f :: Nat -> SNat n
f Z = SZ
f (S n) = SN (f n)
This does not typecheck, because, as i understand, ghc can't infer type n.
Is
it possible to do this at all?
[1]:
https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell#ordinals
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/beginners/attachments/20160411/19222f45/attachment-0001.html>
More information about the Beginners
mailing list