4

There's a number of Haskell modular arithmetic modules that implement type safe modular arithmetic with type annotations. Is it possible to pass in a variable in the type annotation?

For example in the mod module the following works

let x = 4 :: Mod 7
let y = 5 :: Mod 7
print x + y

Is there any way to achieve something similar to the following 

let base = 7
let x = 4 :: Mod base
let y = 5 :: Mod base
print x + y

My problem here is that base is not a type. I'm unsure of the correct way to approach this problem or whether I'm thinking about this in the wrong way for functional languages. Thanks.

Update

In practice base will be the result of some computation I do not know in advance.

notmeduo
  • 51
  • 5
  • What exactly are you trying to achieve here? For the specific example you gave, you don’t need to define a separate `base`, since `base` is just a constant in your example. – bradrn May 23 '20 at 10:17
  • 4
    You're not thinking about this the wrong way for functional languages _in general_; only for Haskell in particular. You're looking for "dependent types", which are a very natural way of thinking about and expressing many mathematical things, and which some functional languages _do_ support. Take a look at languages like Agda and Lean if you're interested. The catch (and it's a big one) is that in the presence of dependent types, type checking can become undecidable, requiring the developer to provide proofs to aid the type checker. – Mark Dickinson May 23 '20 at 11:20
  • 1
    See also https://wiki.haskell.org/Dependent_type – Mark Dickinson May 23 '20 at 11:22
  • @bradrn In practice base will be the output of another function, for example the size of an external file. I was trying to give a minimal example in this case, maybe too minimal... – notmeduo May 23 '20 at 12:27
  • 3
    @notmeduo If `base` is generated by the program, then you’ll want to use [`someNatVal :: Natural -> SomeNat`](http://hackage.haskell.org/package/base-4.12.0.0/docs/GHC-TypeNats.html#v:someNatVal) to convert your value into a type-level natural. That will then let you create and manipulate a `Mod` with the generated base, albeit under an existential — you’ll probably need to define some variant of `newtype SomeMod = forall b. SomeMod (Mod b)`. (1/2) – bradrn May 23 '20 at 13:16
  • (2/2) @notmeduo Also, if you want to do any more complex manipulation than that, you may also want to look into the [`singletons`](http://hackage.haskell.org/package/singletons) package. – bradrn May 23 '20 at 13:16

2 Answers2

1

A value parameterized by the base is a polymorphic value:

import Data.Mod
import GHC.TypeNats (Nat)

nine :: KnownNat base => Mod base
nine =
  let x = 4
      y = 5
  in x + y   -- Let type inference do the work of deducing that x, y :: Mod base

To explicitly annotate these expressions, use ScopedTypeVariables to be able to refer to the base type variable. This also requires base to be explicitly quantified:

{-# LANGUAGE ScopedTypeVariables #-}
import Data.Mod
import GHC.TypeNats (Nat)

nine :: forall base. KnownNat base => Mod base
nine =
  let x = 4 :: Mod base
      y = 5 :: Mod base
  in x + y
Li-yao Xia
  • 31,896
  • 2
  • 33
  • 56
  • I’m not sure how this answers the question. As indicated in the comments, OP seems to want to generate the `base` value at run-time and then lift it to the type level. Certainly I’m sure `-XScopedTypeVariables` will be used _somewhere_ in that process, but in and of itself I don’t think this makes up a full answer. – bradrn May 23 '20 at 14:52
  • @bradm That's some pretty harsh feedback. I'm providing a partial answer (which technically answers the original post BTW) in the hope that it will help OP refine their question. I'll be happy to clarify further based on that. – Li-yao Xia May 23 '20 at 15:23
  • I hope my edit didn't change the question's meaning in any way, that certainly wasn't my intention. – Will Ness May 23 '20 at 15:28
  • Sorry @Li-yaoXia — I didn’t mean to be harsh, so sorry if my comment ended up sounding that way! I simply wanted to say that I was a bit confused by this answer, but I think my comment ended up sounding more harsher than I intended. (I posted it very late at night in my timezone — I probably shouldn’t do that! But thanks for the reply; now that I’m aware of it, I do see now how this could be a partial answer in the hope it helps OP at least a bit. – bradrn May 24 '20 at 00:37
1

I found a similar question

Can I have an unknown KnownNat?

this can be applied in the given example as

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
module Main where

import GHC.TypeLits
import Data.Proxy
import Data.Mod as M

f x = x + 2

main :: IO ()
main = do
    let y = f 5
    let Just someNat = someNatVal y
    case someNat of
        SomeNat (_ :: Proxy n) -> do
            let x = 4 :: M.Mod n
            let y = 5 :: M.Mod n
            print $ x + y
notmeduo
  • 51
  • 5