Construct a dependent type out of a list in Haskell

Question

I want to write a library in Haskell for Galois fields. A Galois field is defined by its irreducible polynomial. Galois field elements can only be added if they have the same Galois field. I want to lift the polynomial into the type of my Galois field, so that for example a Galois field with the polynomial [1, 2, 3] has a different type than a Galois Field with the polynomial [2, 0, 1]. This way i could assure that only Galois field elements with the same Galois field can be added. Is this possible?

My polynomial data type looks like this:

newtype Polynomial a = Polynomial [a]

My Galois field data type look like this:

data GF irr a = GF {
    irreducible :: irr
  , q :: PrimePower
}

So i want a constructor that takes a polynomial (for example (Polynomial [2, 0, 1])) and gives me a Galois field of the type GF (Polynomial Int) ([2, 0, 1]). I know that [2, 0, 1] is not a valid type but i saw that with Data.Singletons it is possible to create types like

(SCons STrue (SCons SFalse SNil))

for [True, False], but i do not know how to construct types likes these from my list [2, 0, 1] and how the constructor would look like.

Answer 1

As Luke already commented, [2, 0, 1] is actually a valid type.

Prelude> :set -XDataKinds -XPolyKinds 
Prelude> data A x = A deriving Show
Prelude> A :: A [2,0,1]
A

where the number literals are actually type-level Nat literals, and [...] is a lifted version of the list value-constructor to the type kind. This can be made explicit by writing it with “prime-quote syntax”

Prelude> A :: A '[2, 0, 1]
A

...so, this task is actually pretty trivial. You can just use

{-# LANGUAGE DataKinds, KindSignatures #-}

import GHC.TypeLits (Nat)

newtype Polynomial a = Polynomial [a]

data GF (irr :: Polynomial Nat) = GF {q :: PrimePower}

As also said by Luke, keep in mind though that type-level calculations don't work as well as they do in full dependently-typed languages. If you really want to do proof stuff with this, you should consider switching to Idris, Agda or Coq.

Answer 2

It seems that the "lifted" value will be used merely as a tag. For cases in which we only want it to work as a tag, but it's difficult to lift the required value to the type level with DataKinds, a possible alternative consists in attaching to the value a "ghostly" type tag conjured by means of a polymorphic incantation. Consider this helper module:

{-# LANGUAGE RankNTypes #-}
module Named (Named,forgetName,name) where

newtype Named n a = Named a -- don't export the constructor

forgetName :: Named n a -> a
forgetName (Named a) = a

name :: a -> ( forall name. Named name a -> r ) -> r
name x f = f ( Named x ) -- inside the callback, "x" has a "name" type tag attached

And this other module which depends on it:

module GF (Polynomial(..),GF,stuff,makeGF,addGF) where

import Named

newtype Polynomial a = Polynomial [a]

data GF a = GF { -- dont' export the constructor
    _stuff :: Int -- don't export the bare field
}

stuff :: GF a -> Int
stuff (GF x) = x

makeGF :: Named ghost (Polynomial Int) -> Int -> GF ghost
makeGF _ = GF 

addGF :: Named ghost (Polynomial Int) -> GF ghost -> GF ghost -> GF ghost
addGF _ x1 x2 = GF (stuff x1 + stuff x2)

I would be impossible for clients of this module to sum two GF values with different ghostly tags. Their only way of creating ghostly tags is through name, and they don't have the means of re-tagging either the Named values or the GF ones—we carefully hid constructors and bare fields to prevent that. So this would compile:

module Main where

import Named
import GF

main :: IO ()
main = print $
    name (Polynomial [2::Int,3,4]) $ \ghost ->
      let x1 = makeGF ghost 3
          x2 = makeGF ghost 4
       in stuff (addGF ghost x1 x2)

But this wouldn't:

main :: IO ()
main = print $
    name (Polynomial [2::Int,3,4]) $ \ghost1 ->
        name (Polynomial [3::Int]) $ \ghost2 ->
          let x1 = makeGF ghost1 3
              x2 = makeGF ghost2 4
           in stuff (addGF ghost1 x1 x2)