A port of `Fin` and `natToFin` from Idris to Haskell.

1.idr

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

2.hs

{-# 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))