StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p><strong>EDIT:</strong> Rewrote answer. It was getting a little bulky (and a little buggy).</p> <h2>GHC 7.6</h2> <p>Since type level <code>Nat</code>s are somewhat... incomplete (?) in GHC 7.6, the least verbose way of achieving what you want is a combination of GADTs and type families.</p> <pre><code>{-# LANGUAGE GADTs, TypeFamilies #-} module Nats where -- Type level nats data Zero data Succ n -- Value level nats data N n f g where Z :: N Zero (a -> b) a S :: N n f g -> N (Succ n) f (a -> g) type family Compose n f g type instance Compose Zero (a -> b) a = b type instance Compose (Succ n) f (a -> g) = a -> Compose n f g compose :: N n f g -> f -> g -> Compose n f g compose Z f x = f x compose (S n) f g = compose n f . g </code></pre> <p>The advantage of this particular implementation is that it doesn't use type classes, so applications of <code>compose</code> aren't subject to the monomorphism restriction. For example, <code>compBinRel = compose (S (S Z)) not</code> will type check without type annotations.</p> <p>We can make this nicer with a little Template Haskell:</p> <pre><code>{-# LANGUAGE TemplateHaskell #-} module Nats.TH where import Language.Haskell.TH nat :: Integer -> Q Exp nat 0 = conE 'Z nat n = appE (conE 'S) (nat (n - 1)) </code></pre> <p>Now we can write <code>compBinRel = compose $(nat 2) not</code>, which is much more pleasant for larger numbers. Some may consider this "cheating", but seeing as we're just implementing a little syntactic sugar, I think it's alright :)</p> <h2>GHC 7.8</h2> <p>The following works on GHC 7.8:</p> <pre><code>-- A lot more extensions. {-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, GADTs, MultiParamTypeClasses, PolyKinds, TypeFamilies, TypeOperators, UndecidableInstances #-} module Nats where import GHC.TypeLits data N = Z | S N data P n = P type family Index n where Index 0 = Z Index n = S (Index (n - 1)) -- Compose is defined using Z/S instead of 0, 1, ... in order to avoid overlapping. class Compose n f r where type Return n f r type Replace n f r compose' :: P n -> (Return n f r -> r) -> f -> Replace n f r instance Compose Z a b where type Return Z a b = a type Replace Z a b = b compose' _ f x = f x instance Compose n f r => Compose (S n) (a -> f) r where type Return (S n) (a -> f) r = Return n f r type Replace (S n) (a -> f) r = a -> Replace n f r compose' x f g = compose' (prev x) f . g where prev :: P (S n) -> P n prev P = P compose :: Compose (Index n) f r => P n -> (Return (Index n) f r -> r) -> f -> Replace (Index n) f r compose x = compose' (convert x) where convert :: P n -> P (Index n) convert P = P -- This does not type check without a signature due to the monomorphism restriction. compBinRel :: (a -> a -> Bool) -> (a -> a -> Bool) compBinRel = compose (P::P 2) not -- This is an example where we compose over higher order functions. -- Think of it as composing (a -> (b -> c)) and ((b -> c) -> c). -- This will not typecheck without signatures, despite the fact that it has arguments. -- However, it will if we use the first solution. appSnd :: b -> (a -> b -> c) -> a -> c appSnd x f = compose (P::P 1) ($ x) f </code></pre> <p>However, this implementation has a few downsides, as annotated in the source.</p> <p>I attempted (and failed) to use closed type families to infer the composition index automatically. It <em>might</em> have been possible to infer higher order functions like this:</p> <pre><code>-- Given r and f, where f = x1 -> x2 -> ... -> xN -> r, Infer r f returns N. type family Infer r f where Infer r r = Zero Infer r (a -> f) = Succ (Infer r f) </code></pre> <p>However, <code>Infer</code> won't work for higher order functions with polymorphic arguments. For example:</p> <pre><code>ghci> :kind! forall a b. Infer a (b -> a) forall a b. Infer a (b -> a) :: * = forall a b. Infer a (b -> a) </code></pre> <p>GHC can't expand <code>Infer a (b -> a)</code> because it doesn't perform an occurs check when matching closed family instances. GHC won't match the second case of <code>Infer</code> on the off chance that <code>a</code> and <code>b</code> are instantiated such that <code>a</code> unifies with <code>b -> a</code>.</p>

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