StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

POType-level nats with literals and an injective successor? (N-ary compose)
text
Body
copied!<p>I'm generalizing <a href="https://stackoverflow.com/a/422818/470844">this <code>n</code>-ary complement</a> to an <code>n</code>-ary compose, but I'm having trouble making the interface nice. Namely, I can't figure out how to use numeric literals at the type level while still being able to pattern match on successors.</p> <h1>Rolling my own nats</h1> <p>Using roll-my-own nats, I can make <code>n</code>-ary compose work, but I can only pass <code>n</code> as an iterated successor, not as a literal:</p> <pre><code>{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE ScopedTypeVariables #-} module RollMyOwnNats where import Data.List (genericIndex) -- import Data.Proxy data Proxy (n::Nat) = Proxy ---------------------------------------------------------------- -- Stuff that works. data Nat = Z | S Nat class Compose (n::Nat) b b' t t' where compose :: Proxy n -> (b -> b') -> t -> t' instance Compose Z b b' b b' where compose _ f x = f x instance Compose n b b' t t' => Compose (S n) b b' (a -> t) (a -> t') where compose _ g f x = compose (Proxy::Proxy n) g (f x) -- Complement a binary relation. compBinRel :: (a -> a -> Bool) -> (a -> a -> Bool) compBinRel = compose (Proxy::Proxy (S (S Z))) not ---------------------------------------------------------------- -- Stuff that does not work. instance Num Nat where fromInteger n = iterate S Z `genericIndex` n -- I now have 'Nat' literals: myTwo :: Nat myTwo = 2 -- But GHC thinks my type-level nat literal is a 'GHC.TypeLits.Nat', -- even when I say otherwise: compBinRel' :: (a -> a -> Bool) -> (a -> a -> Bool) compBinRel' = compose (Proxy::Proxy (2::Nat)) not {- Kind mis-match An enclosing kind signature specified kind `Nat', but `2' has kind `GHC.TypeLits.Nat' In an expression type signature: Proxy (2 :: Nat) In the first argument of `compose', namely `(Proxy :: Proxy (2 :: Nat))' In the expression: compose (Proxy :: Proxy (2 :: Nat)) not -} </code></pre> <h1>Using <code>GHC.TypeLits.Nat</code></h1> <p>Using <code>GHC.TypeLits.Nat</code>, I get type-level nat literals, but there is no successor constructor that I can find, and using the type function <code>(1 +)</code> doesn't work, because GHC (7.6.3) can't reason about injectivity of type functions:</p> <pre><code>{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} module UseGHCTypeLitsNats where import GHC.TypeLits -- import Data.Proxy data Proxy (t::Nat) = Proxy ---------------------------------------------------------------- -- Stuff that works. class Compose (n::Nat) b b' t t' where compose :: Proxy n -> (b -> b') -> t -> t' instance Compose 0 b b' b b' where compose _ f x = f x instance (Compose n b b' t t' , sn ~ (1 + n)) => Compose sn b b' (a -> t) (a -> t') where compose _ g f x = compose (Proxy::Proxy n) g (f x) ---------------------------------------------------------------- -- Stuff that does not work. -- Complement a binary relation. compBinRel , compBinRel' :: (a -> a -> Bool) -> (a -> a -> Bool) compBinRel = compose (Proxy::Proxy 2) not {- Couldn't match type `1 + (1 + n)' with `2' The type variable `n' is ambiguous Possible fix: add a type signature that fixes these type variable(s) In the expression: compose (Proxy :: Proxy 2) not In an equation for `compBinRel': compBinRel = compose (Proxy :: Proxy 2) not -} {- No instance for (Compose n Bool Bool Bool Bool) arising from a use of `compose' The type variable `n' is ambiguous Possible fix: add a type signature that fixes these type variable(s) Note: there is a potential instance available: instance Compose 0 b b' b b' -} compBinRel' = compose (Proxy::Proxy (1+(1+0))) not {- Couldn't match type `1 + (1 + 0)' with `1 + (1 + n)' NB: `+' is a type function, and may not be injective The type variable `n' is ambiguous Possible fix: add a type signature that fixes these type variable(s) Expected type: Proxy (1 + (1 + 0)) Actual type: Proxy (1 + (1 + n)) In the first argument of `compose', namely `(Proxy :: Proxy (1 + (1 + 0)))' -} </code></pre> <p>I agree that <a href="https://stackoverflow.com/a/415154/470844">semantic editor combinators</a> are more elegant and more general here -- and concretely, it will always be easy enough to write <code>(.) . (.) . ...</code> (<code>n</code> times) instead of <code>compose (Proxy::Proxy n)</code> -- but I'm frustrated that I can't make the <code>n</code>-ary composition work as well as I expected. Also, it seems I would run into similar problems for other uses of <code>GHC.TypeLits.Nat</code>, e.g. when trying to define a type function:</p> <pre><code>type family T (n::Nat) :: * type instance T 0 = ... type instance T (S n) = ... </code></pre> <h1>UPDATE: Summary and adaptation of the accepted answer</h1> <p>There's a lot of interesting stuff going on in the accepted answer, but the key for me is the Template Haskell trick in the GHC 7.6 solution: that effectively lets me add type-level literals to my GHC 7.6.3 version, which already had injective successors.</p> <p>Using my types above, I define literals via TH:</p> <pre><code>{-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE DataKinds #-} module RollMyOwnLiterals where import Language.Haskell.TH data Nat = Z | S Nat nat :: Integer -> Q Type nat 0 = [t| Z |] nat n = [t| S $(nat (n-1)) |] </code></pre> <p>where I've moved my <code>Nat</code> declaration into the new module to avoid an import loop. I then modify my <code>RollMyOwnNats</code> module:</p> <pre><code>+import RollMyOwnLiterals ... -data Nat = Z | S Nat ... +compBinRel'' :: (a -> a -> Bool) -> (a -> a -> Bool) +compBinRel'' = compose (Proxy::Proxy $(nat 2)) not </code></pre>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload