Skip to content

Instantly share code, notes, and snippets.

@NathanHowell NathanHowell/1.idr
Last active Mar 23, 2016

Embed
What would you like to do?
A port of `Fin` and `natToFin` from Idris to Haskell.
module Data.Fin
%default total
%access public export
||| Numbers strictly less than some bound. The name comes from "finite sets".
|||
||| It's probably not a good idea to use `Fin` for arithmetic, and they will be
||| exceedingly inefficient at run time.
||| @ n the upper bound
data Fin : (n : Nat) -> Type where
FZ : Fin (S k)
FS : Fin k -> Fin (S k)
-- Construct a Fin from an integer literal which must fit in the given Fin
natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
natToFin Z (S j) = Just FZ
natToFin (S k) (S j) with (natToFin k j)
| Just k' = Just (FS k')
| Nothing = Nothing
natToFin _ _ = Nothing
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Fin where
import Data.Proxy
import GHC.TypeLits
import Numeric.Natural
-- |
-- Define the constructors in terms of minus instead of plus.
-- Makes for more pleasant type signatures later on due to
-- the limited ability of the current TypeNats solver.
-- However this is unsound, as @copumpkin pointed out.
data Fin (n :: Nat) where
FZ :: Fin k
FS :: Fin (k - 1) -> Fin k
deriving instance Show (Fin n)
-- |
-- Create a data kind that we will use to break overlapping
-- instances apart via a closed type family
data Terminate = Definitely | Possibly
-- |
-- We want to stop instance recursion when 0 is reached
type family Guard (n :: Nat) :: Terminate where
Guard 0 = 'Definitely
Guard n = 'Possibly
-- |
-- A naive port of the Idris code to Haskell using a single
-- function rather than a typeclass will blow up the context
-- stack, leading to a compile time error. This is because
-- there is no type level proof that the function will terminate
-- when @k ~ 0@. Making this more explicit satiates GHC.
class NatToFin (b :: Terminate) (k :: Nat) where
natToFin' :: Natural -> Proxy b -> Maybe (Fin k)
-- |
-- Terminate when @k ~ 0@
instance NatToFin 'Definitely 0 where
natToFin' _ _ = Nothing
-- |
-- Decisions need to be made when @k > 0@
instance (KnownNat k, NatToFin (Guard (k - 1)) (k - 1)) => NatToFin 'Possibly k where
-- | The base case: @0 < k@ by virtue of this instance being selected
natToFin' 0 _ =
Just (FZ :: Fin k)
-- | Ensure that @n < k@, recurse then add a 'FS' to the result
natToFin' n _ | toInteger n < natVal (Proxy :: Proxy k) =
FS <$> natToFin' (n - 1) (Proxy :: Proxy (Guard (k - 1)))
-- | If @n >= k@ we fail
natToFin' _ _ = Nothing
-- | Hide the 'Guard' usage behind a nicer type signature
natToFin :: forall k . NatToFin (Guard k) k => Natural -> Maybe (Fin k)
natToFin n = natToFin' n (Proxy :: Proxy (Guard k))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.