Time in Idris

import Data.Time
import Data.Time.Clock
import Data.Time.Calendar
import System.Clock

main : IO ()
main = do
    let p = putStrLn

    -- We'll start by getting the current time.
    now <- getCurrentTime
    p $ show now

    -- You can build a UTCTime by providing the date and time components.
    let then = UTCTime (fromGregorian 2009 11 17) (timeOfDayToTime $ TimeOfDay 20 34 58.651387237)
    p $ show then

    -- You can extract the various components of the time value as expected.
    p $ show $ utctYear $ utctDay then
    p $ show $ utctMonth $ utctDay then
    p $ show $ utctDay $ utctDay then
    p $ show $ todHour $ timeToTimeOfDay $ utctDayTime then
    p $ show $ todMin $ timeToTimeOfDay $ utctDayTime then
    p $ show $ todSec $ timeToTimeOfDay $ utctDayTime then
    p $ show $ picosecondsToDiffTime $ picosecondsToDiffTime $ utctDayTime then

    -- The day of the week is also available.
    p $ show $ dayOfWeek $ utctDay then

    -- These functions compare two times, testing if the first occurs before, after, or at the same time as the second, respectively.
    p $ show $ then < now
    p $ show $ then > now
    p $ show $ then == now

    -- The `diffUTCTime` function returns a NominalDiffTime representing the interval between two times.
    let diff = diffUTCTime now then
    p $ show diff

    -- We can compute the length of the duration in various units.
    p $ show $ nominalDiffTimeToSeconds diff
    p $ show $ nominalDiffTimeToMinutes diff
    p $ show $ nominalDiffTimeToHours diff

    -- You can use `addUTCTime` to advance a time by a given duration, or with a negative duration to move backwards.
    p $ show $ addUTCTime diff then
    p $ show $ addUTCTime (negate diff) then

This Idris code demonstrates working with time and durations. Here’s an explanation of the key differences and adaptations:

Idris uses Data.Time, Data.Time.Clock, and Data.Time.Calendar modules for time-related operations.
Instead of time.Now(), we use getCurrentTime.
To create a specific time, we use UTCTime constructor with fromGregorian for the date and TimeOfDay for the time.
Extracting components of time is done using various functions like utctYear, utctMonth, etc.
Day of the week is obtained using dayOfWeek function.
Time comparisons are done using standard comparison operators (<, >, ==).
diffUTCTime is used to get the time difference, which returns a NominalDiffTime.
Duration calculations are done using functions like nominalDiffTimeToSeconds, nominalDiffTimeToMinutes, etc.
addUTCTime is used to add or subtract durations from a time.

Note that Idris’s time handling is somewhat different from Go’s, but this code achieves similar functionality. The exact output may differ due to the different representations of time and duration in Idris.

Xml in Idris

Sha256 Hashes in Idris

Learn X By Example

Title here

Time in Idris